:: Multivariate polynomials with arbitrary number of variables
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 22, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, ZFMISC_1, RLVECT_1, ALGSTR_0, VECTSP_1,
XBOOLE_0, SUPINF_2, MESFUNC1, SUBSET_1, RELAT_1, FINSEQ_1, ARYTM_3,
PARTFUN1, TARSKI, CARD_3, NAT_1, ORDINAL4, FUNCT_1, FVSUM_1, ALGSTR_1,
BINOP_1, LATTICES, PRE_POLY, ALGSEQ_1, FINSET_1, ARYTM_1, FUNCOP_1,
GROUP_1, FUNCT_4, ORDINAL1, XXREAL_0, FINSEQ_2, MEMBER_1, FUNCT_2,
CARD_1, POLYNOM1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, PBOOLE, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, FINSEQ_1,
STRUCT_0, ALGSTR_0, FUNCT_3, XCMPLX_0, XXREAL_0, BINOP_1, NAT_1,
ALGSTR_1, RLVECT_1, FINSEQ_2, GROUP_1, VECTSP_1, FUNCOP_1, FUNCT_7,
MATRLIN, VFUNCT_1, FVSUM_1, PRE_POLY, RECDEF_1;
constructors BINOP_1, FINSEQOP, FINSEQ_4, RFUNCT_3, FUNCT_7, ALGSTR_1,
FVSUM_1, MATRLIN, RECDEF_1, RELSET_1, PBOOLE, VFUNCT_1, GROUP_1,
PRE_POLY;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, CARD_1,
MEMBERED, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, VALUED_0,
PRE_POLY, RELSET_1, VFUNCT_1, FUNCT_2, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, RLVECT_1, VECTSP_1, GROUP_1,
STRUCT_0, ALGSTR_0;
equalities XBOOLE_0, FINSEQ_2, STRUCT_0, ALGSTR_0, FUNCOP_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, VECTSP_1;
theorems FUNCT_1, FINSET_1, FINSEQ_3, FINSEQ_4, ZFMISC_1, FINSEQ_1, FUNCT_2,
RLVECT_1, VECTSP_1, FUNCOP_1, TARSKI, FUNCT_7, BINOP_1, RELAT_1, MATRLIN,
FINSEQ_2, ORDINAL1, FINSEQ_5, NAT_1, PBOOLE, FVSUM_1, FUNCT_3, GROUP_1,
XBOOLE_0, XBOOLE_1, RLVECT_2, PARTFUN1, XREAL_1, XXREAL_0, PRE_POLY,
VFUNCT_1;
schemes FRAENKEL, FUNCT_2, FINSEQ_2, FINSEQ_1, FINSEQ_4, XBOOLE_0, BINOP_1,
SUBSET_1;
begin
registration
cluster degenerated -> trivial
for add-associative right_zeroed right_complementable
right_unital right-distributive non empty doubleLoopStr;
coherence
proof
let L be add-associative right_zeroed right_complementable right_unital
right-distributive non empty doubleLoopStr such that
A1: 0.L = 1.L;
let u be Element of L;
thus u = u*1.L
.= 0.L by A1;
end;
end;
registration
cluster non trivial -> non degenerated
for add-associative right_zeroed right_complementable
right_unital right-distributive non empty doubleLoopStr;
coherence;
end;
theorem Th1:
for K being non empty addLoopStr, p1,p2 be FinSequence of the
carrier of K st dom p1 = dom p2 holds dom(p1+p2) = dom p1
proof
let K be non empty addLoopStr, p1,p2 be FinSequence of the carrier of K;
assume
A1: dom p1 = dom p2;
A2: rng <:p1,p2:> c= [:rng p1,rng p2:] & [:rng p1,rng p2:] c= [:the carrier
of K,the carrier of K:] by FUNCT_3:51,ZFMISC_1:96;
A3: [:the carrier of K,the carrier of K:] = dom (the addF of K) by
FUNCT_2:def 1;
thus dom (p1+p2) = dom ((the addF of K).:(p1,p2)) by FVSUM_1:def 3
.= dom <:p1,p2:> by A2,A3,RELAT_1:27,XBOOLE_1:1
.= dom p1 /\ dom p2 by FUNCT_3:def 7
.= dom p1 by A1;
end;
theorem Th2:
for L being non empty addLoopStr, F being FinSequence of (the
carrier of L)* holds dom Sum F = dom F
proof
let L be non empty addLoopStr, F be FinSequence of (the carrier of L)*;
len Sum F = len F by MATRLIN:def 6;
hence thesis by FINSEQ_3:29;
end;
theorem Th3:
for L being non empty addLoopStr, F being FinSequence of (the
carrier of L)* holds Sum (<*>((the carrier of L)*)) = <*>(the carrier of L)
proof
let L be non empty addLoopStr, F be FinSequence of (the carrier of L)*;
dom Sum (<*>((the carrier of L)*)) = dom (<*>((the carrier of L)* )) by Th2;
hence thesis;
end;
theorem Th4:
for L being non empty addLoopStr, p being Element of (the
carrier of L)* holds <*Sum p*> = Sum<*p*>
proof
let L be non empty addLoopStr, p be Element of (the carrier of L)*;
A1: now
let i be Nat;
assume i in dom<*p*>;
then i in {1} by FINSEQ_1:2,38;
then
A2: i = 1 by TARSKI:def 1;
hence <*Sum p*>/.i = Sum p by FINSEQ_4:16
.= Sum(<*p*>/.i) by A2,FINSEQ_4:16;
end;
A3: dom <*Sum p*> = Seg 1 by FINSEQ_1:38
.= dom <*p*> by FINSEQ_1:38;
then len <*Sum p*> = len <*p*> by FINSEQ_3:29;
hence thesis by A3,A1,MATRLIN:def 6;
end;
theorem Th5:
for L being non empty addLoopStr, F,G being FinSequence of (the
carrier of L)* holds Sum(F^G) = Sum F ^ Sum G
proof
let L be non empty addLoopStr, F, G be FinSequence of (the carrier of L)*;
A1: dom Sum F = dom F by Th2;
A2: dom Sum G = dom G by Th2;
A3: len (Sum F^Sum G) = len Sum F + len Sum G by FINSEQ_1:22
.= len F + len Sum G by A1,FINSEQ_3:29
.= len F + len G by A2,FINSEQ_3:29
.= len (F^G) by FINSEQ_1:22;
then
A4: dom (Sum F^Sum G) = dom (F^G) by FINSEQ_3:29;
A5: len Sum F = len F by A1,FINSEQ_3:29;
now
let i be Nat such that
A6: i in dom (F^G);
per cases by A6,FINSEQ_1:25;
suppose
A7: i in dom F;
thus (Sum F^Sum G)/.i = (Sum F^Sum G).i by A4,A6,PARTFUN1:def 6
.= (Sum F).i by A1,A7,FINSEQ_1:def 7
.= (Sum F)/.i by A1,A7,PARTFUN1:def 6
.= Sum (F/.i) by A1,A7,MATRLIN:def 6
.= Sum((F^G)/.i) by A7,FINSEQ_4:68;
end;
suppose
ex n being Nat st n in dom G & i = len F + n;
then consider n being Nat such that
A8: n in dom G and
A9: i = len F + n;
thus (Sum F^Sum G)/.i = (Sum F^Sum G).i by A4,A6,PARTFUN1:def 6
.= (Sum G).n by A2,A5,A8,A9,FINSEQ_1:def 7
.= (Sum G)/.n by A2,A8,PARTFUN1:def 6
.= Sum(G/.n) by A2,A8,MATRLIN:def 6
.= Sum((F^G)/.i) by A8,A9,FINSEQ_4:69;
end;
end;
hence thesis by A3,A4,MATRLIN:def 6;
end;
definition
let L be non empty multMagma, p be FinSequence of the carrier of L,
a be Element of L;
redefine func a*p means :: redefines * (FVSUM_1, definition)
:Def1:
dom it = dom p & for i being object st i in dom p holds it/.i = a*(p/.i);
compatibility
proof
A1: now
set R = (a multfield)*p;
let G be FinSequence of the carrier of L;
assume that
A2: dom G = dom p and
A3: for i being object st i in dom p holds G/.i = a*(p/.i);
A4: for k being object st k in dom G holds G.k = R.k
proof
let k be object;
assume
A5: k in dom G;
then G.k = G/.k by PARTFUN1:def 6
.= a*(p/.k) by A2,A3,A5
.= (a multfield).(p/.k) by FVSUM_1:49
.= (a multfield).(p.k) by A2,A5,PARTFUN1:def 6
.= R.k by A2,A5,FUNCT_1:13;
hence thesis;
end;
rng p c= the carrier of L & dom (a multfield) = the carrier of L by
FUNCT_2:def 1;
then dom G = dom R by A2,RELAT_1:27;
then G = R by A4;
hence G = a * p by FVSUM_1:def 6;
end;
set F = a*p;
A6: rng p c= dom (a multfield)
proof
let x be object;
dom (a multfield) = the carrier of L by FUNCT_2:def 1;
hence thesis;
end;
A7: F = (a multfield)*p by FVSUM_1:def 6;
then
A8: dom F = dom p by A6,RELAT_1:27;
for i being object st i in dom p holds F/.i = a*(p/.i)
proof
let i be object;
assume
A9: i in dom p;
F.i = ((a multfield)*p).i by FVSUM_1:def 6
.= (a multfield).(p.i) by A9,FUNCT_1:13
.= (a multfield).(p/.i) by A9,PARTFUN1:def 6
.= a * (p/.i) by FVSUM_1:49;
hence thesis by A8,A9,PARTFUN1:def 6;
end;
hence thesis by A7,A6,A1,RELAT_1:27;
end;
end;
definition
let L be non empty multMagma, p be FinSequence of the carrier of L, a be
Element of L;
func p*a -> FinSequence of the carrier of L means
:Def2:
dom it = dom p & for i being object st i in dom p holds it/.i = (p/.i)*a;
existence
proof
deffunc F(set) = (p/.$1)*a;
consider f being FinSequence of the carrier of L such that
A1: len f = len p and
A2: for j being Nat st j in dom f holds f/.j = F(j) from FINSEQ_4:sch
2;
take f;
thus dom f = dom p by A1,FINSEQ_3:29;
hence thesis by A2;
end;
uniqueness
proof
let it1, it2 be FinSequence of the carrier of L such that
A4: dom it1 = dom p and
A5: for i being object st i in dom p holds it1/.i = (p/.i)*a and
A6: dom it2 = dom p and
A7: for i being object st i in dom p holds it2/.i = (p/.i)*a;
now
let j be Nat;
assume
A8: j in dom p;
hence it1/.j = (p/.j)*a by A5
.= it2/.j by A7,A8;
end;
hence thesis by A4,A6,FINSEQ_5:12;
end;
end;
theorem Th6:
for L being non empty multMagma, a being Element of L holds a*
<*>(the carrier of L) = <*>(the carrier of L)
proof
let L be non empty multMagma, a be Element of L;
dom (a*<*>(the carrier of L)) = dom <*>(the carrier of L) by Def1;
hence thesis;
end;
theorem Th7:
for L being non empty multMagma, a being Element of L holds (<*>
the carrier of L)*a = <*>(the carrier of L)
proof
let L be non empty multMagma, a be Element of L;
dom((<*>the carrier of L)*a) = dom <*>(the carrier of L) by Def2;
hence thesis;
end;
theorem Th8:
for L being non empty multMagma, a, b being Element of L holds a
*<*b*> = <*a*b*>
proof
let L be non empty multMagma, a, b be Element of L;
A1: for i being object st i in dom<*b*> holds <*a*b*>/.i = a*(<*b*>/.i)
proof
let i be object;
assume i in dom<*b*>;
then i in {1} by FINSEQ_1:2,38;
then
A2: i = 1 by TARSKI:def 1;
hence <*a*b*>/.i = a*b by FINSEQ_4:16
.= a*(<*b*>/.i) by A2,FINSEQ_4:16;
end;
dom<*a*b*> = Seg 1 by FINSEQ_1:38
.= dom<*b*> by FINSEQ_1:38;
hence thesis by A1,Def1;
end;
theorem Th9:
for L being non empty multMagma, a, b being Element of L holds
<*b*>*a = <*b*a*>
proof
let L be non empty multMagma, a, b be Element of L;
A1: for i being object st i in dom<*b*> holds <*b*a*>/.i = (<*b*>/.i)*a
proof
let i be object;
assume i in dom<*b*>;
then i in {1} by FINSEQ_1:2,38;
then
A2: i = 1 by TARSKI:def 1;
hence <*b*a*>/.i = b*a by FINSEQ_4:16
.= (<*b*>/.i)*a by A2,FINSEQ_4:16;
end;
dom<*b*a*> = Seg 1 by FINSEQ_1:38
.= dom<*b*> by FINSEQ_1:38;
hence thesis by A1,Def2;
end;
theorem Th10:
for L being non empty multMagma, a being Element of L, p, q
being FinSequence of the carrier of L holds a*(p^q) = (a*p)^(a*q)
proof
let L be non empty multMagma, a be Element of L, p, q be FinSequence of the
carrier of L;
A1: dom (a*(p^q)) = dom (p^q) by Def1;
A2: dom (a*q) = dom q by Def1;
then
A3: len (a*q) = len q by FINSEQ_3:29;
A4: dom (a*p) = dom p by Def1;
then
A5: len (a*p) = len p by FINSEQ_3:29;
A6: now
let i be Nat;
assume
A7: i in dom (a*(p^q));
per cases by A1,A7,FINSEQ_1:25;
suppose
A8: i in dom p;
thus (a*(p^q))/.i = a*((p^q)/.i) by A1,A7,Def1
.= a*(p/.i) by A8,FINSEQ_4:68
.= (a*p)/.i by A8,Def1
.= ((a*p)^(a*q))/.i by A4,A8,FINSEQ_4:68;
end;
suppose
ex n being Nat st n in dom q & i = len p+n;
then consider n being Nat such that
A9: n in dom q and
A10: i = len p+n;
thus (a*(p^q))/.i = a*((p^q)/.i) by A1,A7,Def1
.= a*(q/.n) by A9,A10,FINSEQ_4:69
.= (a*q)/.n by A9,Def1
.= ((a*p)^(a*q))/.i by A5,A2,A9,A10,FINSEQ_4:69;
end;
end;
len ((a*p)^(a*q)) = len (a*p) + len (a*q) by FINSEQ_1:22
.= len (p^q) by A5,A3,FINSEQ_1:22;
then dom (a*(p^q)) = dom ((a*p)^(a*q)) by A1,FINSEQ_3:29;
hence thesis by A6,FINSEQ_5:12;
end;
theorem Th11:
for L being non empty multMagma, a being Element of L, p, q
being FinSequence of the carrier of L holds (p^q)*a = (p*a)^(q*a)
proof
let L be non empty multMagma, a be Element of L, p, q be FinSequence of the
carrier of L;
A1: dom ((p^q)*a) = dom (p^q) by Def2;
A2: dom (q*a) = dom q by Def2;
then
A3: len (q*a) = len q by FINSEQ_3:29;
A4: dom (p*a) = dom p by Def2;
then
A5: len (p*a) = len p by FINSEQ_3:29;
A6: now
let i be Nat;
assume
A7: i in dom ((p^q)*a);
per cases by A1,A7,FINSEQ_1:25;
suppose
A8: i in dom p;
thus ((p^q)*a)/.i = ((p^q)/.i)*a by A1,A7,Def2
.= (p/.i)*a by A8,FINSEQ_4:68
.= (p*a)/.i by A8,Def2
.= ((p*a)^(q*a))/.i by A4,A8,FINSEQ_4:68;
end;
suppose
ex n being Nat st n in dom q & i = len p+n;
then consider n being Nat such that
A9: n in dom q and
A10: i = len p+n;
thus (p^q*a)/.i = ((p^q)/.i)*a by A1,A7,Def2
.= (q/.n)*a by A9,A10,FINSEQ_4:69
.= (q*a)/.n by A9,Def2
.= ((p*a)^(q*a))/.i by A5,A2,A9,A10,FINSEQ_4:69;
end;
end;
len ((p*a)^(q*a)) = len (p*a) + len (q*a) by FINSEQ_1:22
.= len (p^q) by A5,A3,FINSEQ_1:22;
then dom ((p^q)*a) = dom ((p*a)^(q*a)) by A1,FINSEQ_3:29;
hence thesis by A6,FINSEQ_5:12;
end;
registration
cluster right_unital for non empty strict multLoopStr_0;
existence
proof
take multEX_0;
thus thesis;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
associative commutative distributive almost_left_invertible well-unital non
trivial for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
theorem Th12:
for L being add-associative right_zeroed right_complementable
right_unital distributive non empty doubleLoopStr, a being Element of L, p
being FinSequence of the carrier of L holds Sum (a*p) = a*Sum p
proof
let L be add-associative right_zeroed right_complementable right_unital
distributive non empty doubleLoopStr, a be Element of L;
set p = <*>(the carrier of L);
defpred P[FinSequence of the carrier of L] means Sum (a*$1) = a*Sum $1;
A1: now
let p be FinSequence of the carrier of L, r be Element of L such that
A2: P[p];
Sum (a*(p^<*r*>)) = Sum ((a*p)^(a*<*r*>)) by Th10
.= Sum (a*p) + Sum (a*<*r*>) by RLVECT_1:41
.= Sum (a*p) + Sum (<*a*r*>) by Th8
.= Sum (a*p) + a*r by RLVECT_1:44
.= a*Sum p + a*Sum<*r*> by A2,RLVECT_1:44
.= a*(Sum p + Sum<*r*>) by VECTSP_1:def 7
.= a*Sum (p^<*r*>) by RLVECT_1:41;
hence P[p^<*r*>];
end;
Sum p = 0.L & Sum (a*p) = Sum p by Th6,RLVECT_1:43;
then
A3: P[p];
thus for p being FinSequence of the carrier of L holds P[p] from FINSEQ_2:
sch 2(A3,A1);
end;
theorem Th13:
for L being add-associative right_zeroed right_complementable
right_unital distributive non empty doubleLoopStr, a being Element of L, p
being FinSequence of the carrier of L holds Sum (p*a) = (Sum p)*a
proof
let L be add-associative right_zeroed right_complementable right_unital
distributive non empty doubleLoopStr, a be Element of L;
set p = <*>(the carrier of L);
defpred P[FinSequence of the carrier of L] means Sum ($1*a) = (Sum $1)*a;
A1: now
let p be FinSequence of the carrier of L, r be Element of L such that
A2: P[p];
Sum ((p^<*r*>)*a) = Sum ((p*a)^(<*r*>*a)) by Th11
.= Sum (p*a) + Sum (<*r*>*a) by RLVECT_1:41
.= Sum (p*a) + Sum (<*r*a*>) by Th9
.= Sum (p*a) + r*a by RLVECT_1:44
.= (Sum p)*a + (Sum<*r*>)*a by A2,RLVECT_1:44
.= (Sum p + Sum<*r*>)*a by VECTSP_1:def 7
.= (Sum (p^<*r*>))*a by RLVECT_1:41;
hence P[p^<*r*>];
end;
Sum p = 0.L & Sum (p*a) = Sum p by Th7,RLVECT_1:43;
then
A3: P[p];
thus for p being FinSequence of the carrier of L holds P[p] from FINSEQ_2:
sch 2(A3,A1);
end;
begin :: Sequence flattening --------------------------------------------------
theorem Th14:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr, F being FinSequence of (the carrier of L)* holds Sum
FlattenSeq F = Sum Sum F
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr;
defpred P[FinSequence of (the carrier of L)*] means Sum FlattenSeq $1 = Sum
Sum $1;
A1: for f being FinSequence of (the carrier of L)*, p being Element of (the
carrier of L)* st P[f] holds P[f^<*p*>]
proof
let f be FinSequence of (the carrier of L)*, p be Element of (the carrier
of L)* such that
A2: Sum FlattenSeq f = Sum Sum f;
thus Sum FlattenSeq(f^<*p*>) = Sum((FlattenSeq f)^FlattenSeq <*p*>) by
PRE_POLY:3
.= Sum((FlattenSeq f)^p) by PRE_POLY:1
.= Sum Sum f +Sum p by A2,RLVECT_1:41
.= Sum Sum f+Sum<*Sum p*> by RLVECT_1:44
.= Sum(Sum f^<*Sum p*>) by RLVECT_1:41
.= Sum(Sum f^Sum<*p*>) by Th4
.= Sum Sum(f^<*p*>) by Th5;
end;
Sum FlattenSeq(<*>((the carrier of L)*)) = Sum <*>(the carrier of L);
then
A3: P[<*>((the carrier of L)*)] by Th3;
thus for f be FinSequence of (the carrier of L)* holds P[f] from FINSEQ_2:
sch 2(A3,A1);
end;
definition
let S be ZeroStr, f be (the carrier of S)-valued Function;
func Support f -> set means
:Def3:
for x being object holds x in it iff x in dom f & f.x <> 0.S;
existence
proof
defpred P[object] means f.$1 <> 0.S;
consider X being set such that
A1: for x being object holds x in X iff x in dom f & P[x] from XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
let A,B be set such that
A2: for x being object holds x in A iff x in dom f & f.x <> 0.S and
A3: for x being object holds x in B iff x in dom f & f.x <> 0.S;
now
let x be object;
x in A iff x in dom f & f.x <> 0.S by A2;
hence x in A iff x in B by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X be non empty set, S be non empty ZeroStr, f be Function of X, S;
redefine func Support f -> Subset of X means :: redefines Support (POLYNOM1, definition)
:Def4:
for x being Element of X holds x in it iff f.x <> 0.S;
coherence
proof
Support f c= dom f
by Def3;
hence Support f is Subset of X by XBOOLE_1:1;
end;
compatibility
proof let A be Subset of X;
A1: X = dom f by PARTFUN1:def 2;
hence A = Support f implies
for x being Element of X holds x in A iff f.x <> 0.S by Def3;
assume
A2: for x being Element of X holds x in A iff f.x <> 0.S;
A3: Support f c= dom f
by Def3;
thus A c= Support f
proof let e be object;
assume
A4: e in A;
then
f.e <> 0.S by A2;
hence e in Support f by A4,A1,Def3;
end;
let e be object;
assume
A5: e in Support f;
then
A6: f.e <> 0.S by Def3;
Support f c= X by A3,XBOOLE_1:1;
hence e in A by A2,A6,A5;
end;
end;
definition
let S be ZeroStr, p be (the carrier of S)-valued Function;
attr p is finite-Support means
:Def5:
Support p is finite;
end;
definition
let n be set, L be non empty 1-sorted, p be Function of Bags n, L, x be bag
of n;
redefine func p.x -> Element of L; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider b = x as Element of Bags n by PRE_POLY:def 12;
reconsider f = p as Function of Bags n, the carrier of L;
f.b is Element of L;
hence thesis;
end;
end;
begin :: Formal power series --------------------------------------------------
definition
let X be set, S be 1-sorted;
mode Series of X, S is Function of Bags X, S;
end;
definition
let n be set, L be non empty addLoopStr, p,q be Series of n, L;
func p+q -> Series of n, L equals
p + q;
coherence;
end;
theorem Th15:
for n being set, L being non empty addLoopStr, p,q being Series of n, L
for x being bag of n holds (p+q).x = p.x + q.x
proof
let n be set;
let L be non empty addLoopStr;
let p, q be Series of n, L;
let x be bag of n;
A1: dom p = Bags n & dom q = Bags n by FUNCT_2:def 1;
A2: x in Bags n by PRE_POLY:def 12;
then
A3: p/.x = p.x & q/.x = q.x by A1,PARTFUN1:def 6;
A4: dom (p+q) = dom p /\ dom q by VFUNCT_1:def 1;
hence (p+q).x = (p+q)/.x by A1,A2,PARTFUN1:def 6
.= p.x + q.x by A1,A2,A3,A4,VFUNCT_1:def 1;
end;
theorem
for n being set, L being non empty addLoopStr, p,q,r being Series of n, L
st for x being bag of n holds r.x = p.x + q.x holds
r = p + q
proof
let n be set;
let L be non empty addLoopStr;
let p,q,r be Series of n, L;
assume
A1: for x being bag of n holds r.x = p.x + q.x;
let x be Element of Bags n;
A2: dom (p+q) = Bags n by FUNCT_2:def 1;
A3: (p+q)/.x = (p+q).x;
A4: p/.x = p.x & q/.x = q.x;
thus r.x = p.x + q.x by A1
.= (p + q).x by A2,A3,A4,VFUNCT_1:def 1;
end;
theorem Th17:
for n being set,
L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being Series of n, L
for x being bag of n holds (-p).x = -(p.x)
proof
let n be set;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p be Series of n, L;
let x be bag of n;
A1: dom p = Bags n by FUNCT_2:def 1;
A2: x in Bags n by PRE_POLY:def 12;
then
A3: p/.x = p.x by A1,PARTFUN1:def 6;
A4: dom (-p) = dom p by VFUNCT_1:def 5;
hence (-p).x = (-p)/.x by A1,A2,PARTFUN1:def 6
.= -p.x by A1,A2,A3,A4,VFUNCT_1:def 5;
end;
theorem
for n being set,
L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p,r being Series of n, L
st for x being bag of n holds r.x = -(p.x) holds
r = -p
proof
let n be set;
let L be add-associative right_zeroed right_complementable
non empty addLoopStr;
let p,r be Series of n, L;
assume
A1: for x being bag of n holds r.x = -p.x;
let x be Element of Bags n;
A2: dom (-p) = Bags n by FUNCT_2:def 1;
A3: (-p)/.x = (-p).x;
A4: p/.x = p.x;
thus r.x = -p.x by A1
.= (-p).x by A2,A3,A4,VFUNCT_1:def 5;
end;
theorem
for n be set, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Series of n, L holds p = - -p
proof
let n be set,L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Series of n, L;
set r = -p;
A1: dom p = Bags n by FUNCT_2:def 1;
A2: dom -p = dom p by VFUNCT_1:def 5;
A3: dom - -p = dom -p by VFUNCT_1:def 5;
now
let x be Element of Bags n;
assume x in dom p;
A4: p.x = p/.x;
thus p.x = - - (p.x) by RLVECT_1:17
.= - ((-p)/.x) by A1,A2,A4,VFUNCT_1:def 5
.= (- -p)/.x by A1,A2,A3,VFUNCT_1:def 5
.= (-r).x;
end;
hence thesis by A1;
end;
theorem Th20:
for n being set, L being right_zeroed non empty addLoopStr, p,
q being Series of n, L holds Support (p+q) c= Support p \/ Support q
proof
let n be set, L be right_zeroed non empty addLoopStr, p, q be Series of n,
L;
set f = p+q, Sp = Support p, Sq = Support q;
let x be object;
assume
A1: x in Support f;
then reconsider x9 = x as Element of Bags n;
f.x9 <> 0.L by A1,Def4;
then p.x9+q.x9 <> 0.L by Th15;
then not(p.x9 = 0.L & q.x9 = 0.L) by RLVECT_1:def 4;
then x9 in Sp or x9 in Sq by Def4;
hence thesis by XBOOLE_0:def 3;
end;
definition
let n be set, L be Abelian right_zeroed non empty addLoopStr, p, q be
Series of n, L;
redefine func p+q; :: redefines + (POLYNOM1, definition)
commutativity
proof
let p, q be Series of n, L;
now
let b be Element of Bags n;
thus (p + q).b = q.b + p.b by Th15
.= (q + p).b by Th15;
end;
hence p+q = q+p;
end;
end;
theorem Th21:
for n being set, L being add-associative right_zeroed non empty
doubleLoopStr, p, q, r being Series of n, L holds (p+q)+r = p+(q+r)
proof
let n be set, L be add-associative right_zeroed non empty doubleLoopStr, p
, q, r be Series of n, L;
now
let b be Element of Bags n;
thus ((p+q)+r).b = (p+q).b+r.b by Th15
.= p.b+q.b+r.b by Th15
.= p.b+(q.b+r.b) by RLVECT_1:def 3
.= p.b+(q+r).b by Th15
.= (p+(q+r)).b by Th15;
end;
hence thesis;
end;
definition
let n be set, L be add-associative right_zeroed right_complementable non
empty addLoopStr, p, q be Series of n, L;
func p-q -> Series of n, L equals
p+-q;
coherence;
end;
definition
let n be set, S be non empty ZeroStr;
func 0_(n, S) -> Series of n, S equals
(Bags n) --> 0.S;
coherence;
end;
theorem Th22:
for n being set, S being non empty ZeroStr, b be bag of n holds
(0_(n, S)).b = 0.S
proof
let n be set, S be non empty ZeroStr, b be bag of n;
b in Bags n by PRE_POLY:def 12;
hence thesis by FUNCOP_1:7;
end;
theorem Th23:
for n being set, L be right_zeroed non empty addLoopStr, p be
Series of n, L holds p+0_(n,L) = p
proof
let n be set, L be right_zeroed non empty addLoopStr, p be Series of n, L;
reconsider ls = p+0_(n,L), p9 = p as Function of (Bags n), the carrier of L;
now
let b be Element of Bags n;
thus ls.b = p.b + 0_(n,L).b by Th15
.= p9.b+0.L
.= p9.b by RLVECT_1:def 4;
end;
hence thesis;
end;
definition
let n be set, L be right_unital non empty multLoopStr_0;
func 1_(n,L) -> Series of n, L equals
0_(n,L)+*(EmptyBag n,1.L);
coherence;
end;
theorem Th24:
for n being set, L being add-associative right_zeroed
right_complementable non empty addLoopStr, p being Series of n, L holds p-p =
0_(n,L)
proof
let n be set, L be add-associative right_zeroed right_complementable non
empty addLoopStr, p be Series of n, L;
reconsider pp = p-p, Z = 0_(n,L) as Function of Bags n, the carrier of L;
now
let b be Element of Bags n;
thus pp.b = p.b+(-p).b by Th15
.= p.b + -p.b by Th17
.= 0.L by RLVECT_1:def 10
.= Z.b;
end;
hence thesis;
end;
theorem Th25:
for n being set, L being right_unital non empty multLoopStr_0
holds (1_(n,L)).EmptyBag n = 1.L & for b being bag of n st b <> EmptyBag n
holds (1_(n,L)).b = 0.L
proof
let n be set, L be right_unital non empty multLoopStr_0;
set Z = 0_(n,L);
dom Z = Bags n;
hence (1_(n,L)).EmptyBag n = 1.L by FUNCT_7:31;
let b be bag of n;
A1: b in Bags n by PRE_POLY:def 12;
assume b <> EmptyBag n;
hence (1_(n,L)).b = Z.b by FUNCT_7:32
.= 0.L by A1,FUNCOP_1:7;
end;
definition
let n be Ordinal, L be add-associative right_complementable right_zeroed
non empty doubleLoopStr, p, q be Series of n, L;
func p*'q -> Series of n, L means
:Def10:
for b being bag of n ex s being
FinSequence of the carrier of L st it.b = Sum s & len s = len decomp b & for k
being Element of NAT st k in dom s ex b1, b2 being bag of n st (decomp b)/.k =
<*b1, b2*> & s/.k = p.b1*q.b2;
existence
proof
defpred P[Element of Bags n, Element of L] means ex b being bag of n st b
= $1 & ex s being FinSequence of the carrier of L st $2 = Sum s & len s = len
decomp b & for k being Element of NAT st k in dom s ex b1, b2 being bag of n st
(decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2;
A1: now
let bb be Element of Bags n;
reconsider b = bb as bag of n;
defpred Q[Nat, set] means ex b1, b2 being bag of n st (decomp b)/.$1 =
<*b1, b2*> & $2 = p.b1*q.b2;
A2: now
let k be Nat;
assume k in Seg len decomp b;
then k in dom decomp b by FINSEQ_1:def 3;
then consider b1, b2 being bag of n such that
A3: (decomp b)/.k = <*b1,b2*> and
b = b1+b2 by PRE_POLY:68;
reconsider x = p.b1*q.b2 as Element of L;
take x;
thus Q[k,x] by A3;
end;
consider s being FinSequence of the carrier of L such that
A4: len s = len decomp b and
A5: for k being Nat st k in Seg len decomp b holds Q[k, s/.k] from
FINSEQ_4:sch 1 (A2);
reconsider y = Sum s as Element of L;
take y;
thus P[bb,y]
proof
take b;
thus b = bb;
take s;
thus y = Sum s;
thus len s = len decomp b by A4;
let k be Element of NAT;
assume k in dom s;
then k in Seg len decomp b by A4,FINSEQ_1:def 3;
hence thesis by A5;
end;
end;
consider P being Function of (Bags n), the carrier of L such that
A6: for b being Element of Bags n holds P[b, P.b] from FUNCT_2:sch 3(
A1);
reconsider P as Function of (Bags n), L;
reconsider P as Series of n, L;
take P;
let b be bag of n;
reconsider bb = b as Element of Bags n by PRE_POLY:def 12;
P[bb, P.bb] by A6;
hence thesis;
end;
uniqueness
proof
let it1, it2 be Series of n, L such that
A7: for b being bag of n ex s being FinSequence of the carrier of L
st it1.b = Sum s & len s = len decomp b & for k being Element of NAT st k in
dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2
and
A8: for b being bag of n ex s being FinSequence of the carrier of L
st it2.b = Sum s & len s = len decomp b & for k being Element of NAT st k in
dom s ex b1, b2 being bag of n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2
;
reconsider ita = it1, itb = it2 as Function of (Bags n), the carrier of L;
now
let b be Element of Bags n;
consider sa being FinSequence of the carrier of L such that
A9: ita.b = Sum sa and
A10: len sa = len decomp b and
A11: for k being Element of NAT st k in dom sa ex b1, b2 being bag
of n st (decomp b)/.k = <*b1, b2*> & sa/.k = p.b1*q.b2 by A7;
consider sb being FinSequence of the carrier of L such that
A12: itb.b = Sum sb and
A13: len sb = len decomp b and
A14: for k being Element of NAT st k in dom sb ex b1, b2 being bag
of n st (decomp b)/.k = <*b1, b2*> & sb/.k = p.b1*q.b2 by A8;
now
let k be Nat;
assume
A15: 1 <= k & k <= len sa;
then
A16: k in dom sa by FINSEQ_3:25;
then
A17: sa/.k = sa.k by PARTFUN1:def 6;
A18: k in dom sb by A10,A13,A15,FINSEQ_3:25;
then
A19: sb/.k = sb.k by PARTFUN1:def 6;
consider ab1, ab2 being bag of n such that
A20: (decomp b)/.k = <*ab1, ab2*> and
A21: sa/.k = p.ab1*q.ab2 by A11,A16;
consider bb1, bb2 being bag of n such that
A22: (decomp b)/.k = <*bb1, bb2*> and
A23: sb/.k = p.bb1*q.bb2 by A14,A18;
ab1 = bb1 by A20,A22,FINSEQ_1:77;
hence sa.k = sb.k by A20,A21,A22,A23,A17,A19,FINSEQ_1:77;
end;
hence ita.b = itb.b by A9,A10,A12,A13,FINSEQ_1:14;
end;
hence it1 = it2;
end;
end;
theorem Th26:
for n being Ordinal, L being Abelian add-associative
right_zeroed right_complementable distributive associative non empty
doubleLoopStr, p, q, r being Series of n, L holds p*'(q+r) = p*'q+p*'r
proof
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable distributive associative non empty doubleLoopStr, p, q,
r be Series of n, L;
set cL = the carrier of L;
now
let b be Element of Bags n;
consider s being FinSequence of cL such that
A1: (p*'(q+r)).b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*(q+r).b2 by Def10;
consider u being FinSequence of cL such that
A4: (p*'r).b = Sum u and
A5: len u = len decomp b and
A6: for k being Element of NAT st k in dom u ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & u/.k = p.b1*r.b2 by Def10;
consider t being FinSequence of cL such that
A7: (p*'q).b = Sum t and
A8: len t = len decomp b and
A9: for k being Element of NAT st k in dom t ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & t/.k = p.b1*q.b2 by Def10;
reconsider t, u as Element of (len s)-tuples_on cL by A2,A8,A5,FINSEQ_2:92;
A10: dom u = dom s by A2,A5,FINSEQ_3:29;
A11: dom t = dom s by A2,A8,FINSEQ_3:29;
then
A12: dom (t+u) = dom s by A10,Th1;
A13: now
let i be Nat;
assume
A14: i in dom s;
then consider sb1, sb2 being bag of n such that
A15: (decomp b)/.i = <*sb1, sb2*> and
A16: s/.i = p.sb1*(q+r).sb2 by A3;
A17: t/.i = t.i & u/.i = u.i by A11,A10,A14,PARTFUN1:def 6;
consider ub1, ub2 being bag of n such that
A18: (decomp b)/.i = <*ub1, ub2*> and
A19: u/.i = p.ub1*r.ub2 by A6,A10,A14;
A20: sb1 = ub1 & sb2 = ub2 by A15,A18,FINSEQ_1:77;
consider tb1, tb2 being bag of n such that
A21: (decomp b)/.i = <*tb1, tb2*> and
A22: t/.i = p.tb1*q.tb2 by A9,A11,A14;
A23: sb1 = tb1 & sb2 = tb2 by A15,A21,FINSEQ_1:77;
s/.i = s.i by A14,PARTFUN1:def 6;
hence s.i = p.sb1*(q.sb2+r.sb2) by A16,Th15
.= p.sb1*q.sb2+p.sb1*r.sb2 by VECTSP_1:def 7
.= (t + u).i by A12,A14,A22,A19,A23,A20,A17,FVSUM_1:17;
end;
len (t+u) = len s by A12,FINSEQ_3:29;
then s = t + u by A13,FINSEQ_2:9;
hence (p*'(q+r)).b = Sum t + Sum u by A1,FVSUM_1:76
.= (p*'q+p*'r).b by A7,A4,Th15;
end;
hence thesis;
end;
theorem Th27:
for n being Ordinal, L being Abelian add-associative
right_zeroed right_complementable right_unital distributive associative non
empty doubleLoopStr, p, q, r being Series of n, L holds (p*'q)*'r = p*'(q*'r)
proof
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable right_unital distributive associative non empty
doubleLoopStr, p, q, r be Series of n, L;
set cL = the carrier of L;
reconsider pqra = (p*'q)*'r, pqrb = p*'(q*'r) as Function of Bags n, cL;
set pq = p*'q, qr = q*'r;
now
let b be Element of Bags n;
set db = decomp b;
deffunc F(Nat) = ((decomp (((db/.$1)/.1) qua Element of Bags n))) ^^ ((len
(decomp (((db/.$1)/.1) qua Element of Bags n)))|-> <*(db/.$1)/.2*>);
consider dbl being FinSequence such that
A1: len dbl = len db and
A2: for k being Nat st k in dom dbl holds dbl.k = F(k) from FINSEQ_1:
sch 2;
A3: rng dbl c= (3-tuples_on Bags n)*
proof
let y be object;
assume y in rng dbl;
then consider k being object such that
A4: k in dom dbl and
A5: y = dbl.k by FUNCT_1:def 3;
reconsider k as set by TARSKI:1;
set dbk2 = (db/.k)/.2;
set ddbk1 = decomp (((db/.k)/.1) qua Element of Bags n);
reconsider k as Nat by A4;
set dblk = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>);
A6: dom dblk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by PRE_POLY:def 4
.= dom ddbk1 /\ Seg len ddbk1
.= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3
.= dom ddbk1;
A7: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3;
rng dblk c= 3-tuples_on Bags n
proof
reconsider Gi = <*dbk2*> as Element of 1-tuples_on Bags n
by FINSEQ_2:98;
let y be object;
assume y in rng dblk;
then consider i being object such that
A8: i in dom dblk and
A9: dblk.i = y by FUNCT_1:def 3;
ddbk1.i in rng ddbk1 by A6,A8,FUNCT_1:def 3;
then reconsider Fi = ddbk1.i as Element of 2-tuples_on Bags n;
reconsider i9 = i as Element of NAT by A8;
((len ddbk1) |-> <*dbk2*>).i9 = <*dbk2*> by A6,A7,A8,FUNCOP_1:7;
then y = Fi^Gi by A8,A9,PRE_POLY:def 4;
hence thesis by FINSEQ_2:131;
end;
then
A10: dblk is FinSequence of 3-tuples_on Bags n by FINSEQ_1:def 4;
dbl.k = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>) by A2,A4;
hence thesis by A5,A10,FINSEQ_1:def 11;
end;
deffunc F(Element of 3-tuples_on Bags n) = p.($1/.1)*q.($1/.2)*r.($1/.3);
consider v being Function of (3-tuples_on Bags n), cL such that
A11: for b being Element of 3-tuples_on Bags n holds v.b = F(b) from
FUNCT_2:sch 4;
deffunc G(Nat) = ((len (decomp (((db/.$1)/.2) qua Element of Bags n))) |->
<*(db/.$1)/.1*>) ^^ ((decomp (((db/.$1)/.2) qua Element of Bags n)));
consider dbr being FinSequence such that
A12: len dbr = len db and
A13: for k being Nat st k in dom dbr holds dbr.k = G(k) from FINSEQ_1:
sch 2;
rng dbr c= (3-tuples_on Bags n)*
proof
let y be object;
assume y in rng dbr;
then consider k being object such that
A14: k in dom dbr and
A15: y = dbr.k by FUNCT_1:def 3;
reconsider k as Nat by A14;
set ddbk1 = decomp (((db/.k)/.2) qua Element of Bags n);
set dbk2 = (db/.k)/.1;
set dbrk = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1;
A16: dom dbrk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by PRE_POLY:def 4
.= dom ddbk1 /\ Seg len ddbk1
.= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3
.= dom ddbk1;
A17: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3;
rng dbrk c= 3-tuples_on Bags n
proof
reconsider Gi = <*dbk2*> as Element of 1-tuples_on Bags n
by FINSEQ_2:98;
let y be object;
assume y in rng dbrk;
then consider i being object such that
A18: i in dom dbrk and
A19: dbrk.i = y by FUNCT_1:def 3;
ddbk1.i in rng ddbk1 by A16,A18,FUNCT_1:def 3;
then reconsider Fi = ddbk1.i as Element of 2-tuples_on Bags n;
reconsider i9 = i as Element of NAT by A18;
((len ddbk1) |-> <*dbk2*>).i9 = <*dbk2*> by A16,A17,A18,FUNCOP_1:7;
then y = Gi^Fi by A18,A19,PRE_POLY:def 4;
hence thesis by FINSEQ_2:131;
end;
then
A20: dbrk is FinSequence of 3-tuples_on Bags n by FINSEQ_1:def 4;
dbr.k = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1 by A13,A14;
hence thesis by A15,A20,FINSEQ_1:def 11;
end;
then reconsider dbl, dbr as FinSequence of (3-tuples_on Bags n)* by A3,
FINSEQ_1:def 4;
set fdbl = FlattenSeq dbl, fdbr = FlattenSeq dbr;
consider ls being FinSequence of cL such that
A21: pqra.b = Sum ls and
A22: len ls = len decomp b and
A23: for k being Element of NAT st k in dom ls ex b1,b2 being bag of n
st db/.k = <*b1,b2*> & ls/.k = pq.b1*r.b2 by Def10;
A24: dom dbr = dom db by A12,FINSEQ_3:29;
reconsider vfdbl = v*fdbl,vfdbr = v*fdbr as FinSequence of cL by
FINSEQ_2:32;
consider vdbl being FinSequence of cL* such that
A25: vdbl = ((dom dbl --> v)**dbl) and
A26: vfdbl = FlattenSeq vdbl by PRE_POLY:32;
A27: dom v = 3-tuples_on Bags n by FUNCT_2:def 1;
now
set f = Sum vdbl;
A28: dom vdbl = dom (dom dbl --> v) /\ dom dbl by A25,PBOOLE:def 19
.= dom dbl /\ dom dbl
.= dom dbl;
A29: dom f = dom vdbl by Th2;
hence len Sum vdbl = len ls by A22,A1,A28,FINSEQ_3:29;
let k be Nat such that
A30: 1 <= k & k <= len ls;
A31: k in dom f by A22,A1,A29,A28,A30,FINSEQ_3:25;
A32: f/.k = f.k by A22,A1,A29,A28,A30,FINSEQ_3:25,PARTFUN1:def 6;
A33: dom ls = dom f by A22,A1,A29,A28,FINSEQ_3:29;
then
A34: ls/.k = ls.k by A30,FINSEQ_3:25,PARTFUN1:def 6;
consider b1,b2 being bag of n such that
A35: db/.k = <*b1,b2*> and
A36: ls/.k = pq.b1*r.b2 by A23,A33,A31;
A37: len <*b1,b2*> = 2 by FINSEQ_1:44;
then 1 in dom <*b1,b2*> by FINSEQ_3:25;
then
A38: (db/.k)/.1 = <*b1,b2*>.1 by A35,PARTFUN1:def 6
.= b1;
set dblk = dbl.k;
set dbk2 = (db/.k)/.2;
set ddbk1 = decomp (((db/.k)/.1) qua Element of Bags n);
A39: k in dom vdbl by A22,A1,A28,A30,FINSEQ_3:25;
then
A40: dbl.k = ddbk1 ^^ ((len ddbk1) |-> <*dbk2*>) by A2,A28;
then
A41: dom dblk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by PRE_POLY:def 4
.= dom ddbk1 /\ Seg len ddbk1
.= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3
.= dom ddbk1;
set vdblk = v*(dbl.k);
k in dom dbl by A22,A1,A30,FINSEQ_3:25;
then dblk in rng dbl by FUNCT_1:def 3;
then dblk is Element of (3-tuples_on Bags n)*;
then reconsider dblk as FinSequence of 3-tuples_on Bags n;
rng dblk c= 3-tuples_on Bags n;
then
A42: dom vdblk = dom dblk by A27,RELAT_1:27;
then
A43: dom vdblk = Seg len ddbk1 by A41,FINSEQ_1:def 3;
reconsider b29 = b2 as Element of Bags n by PRE_POLY:def 12;
consider pqs being FinSequence of the carrier of L such that
A44: pq.b1 = Sum pqs and
A45: len pqs = len decomp b1 and
A46: for i being Element of NAT st i in dom pqs ex b11, b12 being
bag of n st (decomp b1)/.i = <*b11, b12*> & pqs/.i = p.b11*q.b12 by Def10;
A47: dom pqs = dom (pqs*r.b2) by Def2;
2 in dom <*b1,b2*> by A37,FINSEQ_3:25;
then
A48: dbk2 = <*b1,b2*>.2 by A35,PARTFUN1:def 6
.= b2;
reconsider vdblk as FinSequence by A43,FINSEQ_1:def 2;
A49: Sum (pqs*r.b2) = (Sum pqs)*r.b2 by Th13;
A50: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3;
now
A51: dom pqs = dom (pqs*r.b2) by Def2;
thus len vdblk = len pqs by A45,A38,A41,A42,FINSEQ_3:29
.= len (pqs*r.b2) by A47,FINSEQ_3:29;
then
A52: dom vdblk = dom (pqs*r.b2) by FINSEQ_3:29;
let i be Nat;
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
assume
A53: 1 <= i & i <= len (pqs*r.b2);
then
A54: i in dom (pqs*r.b2) by FINSEQ_3:25;
then consider b11, b12 being bag of n such that
A55: (decomp b1)/.i = <*b11, b12*> and
A56: pqs/.i = p.b11*q.b12 by A46,A47;
((len ddbk1) |-> <*dbk2*>).i9 = <*dbk2*> & (decomp b1)/.i = (
decomp b1).i by A38,A41,A50,A42,A52,A54,FUNCOP_1:7,PARTFUN1:def 6;
then
A57: dblk.i = <*b11,b12*>^<*b2*> by A48,A38,A40,A42,A52,A54,A55,
PRE_POLY:def 4
.= <*b11,b12,b2*> by FINSEQ_1:43;
reconsider b119 = b11, b129 = b12 as Element of Bags n
by PRE_POLY:def 12;
reconsider B = <*b119,b129,b29*> as Element of 3-tuples_on Bags n by
FINSEQ_2:104;
A58: i in dom pqs by A47,A53,FINSEQ_3:25;
thus (v*(dbl.k)).i = v.(dblk.i) by A52,A54,FUNCT_1:12
.= p.(B/.1)*q.(B/.2)*r.(B/.3) by A11,A57
.= p.b119*q.(B/.2)*r.(B/.3) by FINSEQ_4:18
.= p.b11*q.b12*r.(B/.3) by FINSEQ_4:18
.= (pqs/.i)*r.b2 by A56,FINSEQ_4:18
.= (pqs*r.b2)/.i by A58,Def2
.= (pqs*r.b2).i by A58,A51,PARTFUN1:def 6;
end;
then
A59: vdblk = pqs*r.b2 by FINSEQ_1:14;
vdbl/.k = vdbl.k by A39,PARTFUN1:def 6
.= ((dom dbl --> v).k)*(dbl.k) by A25,A39,PBOOLE:def 19
.= pqs*r.b2 by A28,A39,A59,FUNCOP_1:7;
hence (Sum vdbl).k = ls.k by A31,A36,A44,A49,A34,A32,MATRLIN:def 6;
end;
then
A60: Sum vdbl = ls by FINSEQ_1:14;
consider vdbr being FinSequence of cL* such that
A61: vdbr = ((dom dbr --> v)**dbr) and
A62: vfdbr = FlattenSeq vdbr by PRE_POLY:32;
A63: Sum vfdbr = Sum Sum vdbr by A62,Th14;
consider rs being FinSequence of cL such that
A64: pqrb.b = Sum rs and
A65: len rs = len decomp b and
A66: for k being Element of NAT st k in dom rs ex b1,b2 being bag of n
st db/.k = <*b1,b2*> & rs/.k = p.b1*qr.b2 by Def10;
now
set f = Sum vdbr;
A67: dom vdbr = dom (dom dbr --> v) /\ dom dbr by A61,PBOOLE:def 19
.= dom dbr /\ dom dbr
.= dom dbr;
A68: dom f = dom vdbr by Th2;
hence len Sum vdbr = len rs by A65,A12,A67,FINSEQ_3:29;
let k be Nat such that
A69: 1 <= k & k <= len rs;
A70: k in dom f by A65,A12,A68,A67,A69,FINSEQ_3:25;
then
A71: f/.k = f.k by PARTFUN1:def 6;
set dbrk = dbr.k;
set dbk2 = (db/.k)/.1;
set ddbk1 = decomp (((db/.k)/.2) qua Element of Bags n);
A72: k in dom vdbr by A65,A12,A67,A69,FINSEQ_3:25;
then
A73: dbr.k = ((len ddbk1) |-> <*dbk2*>) ^^ ddbk1 by A13,A67;
then
A74: dom dbrk = dom ddbk1 /\ dom ((len ddbk1) |-> <*dbk2*>) by PRE_POLY:def 4
.= dom ddbk1 /\ Seg len ddbk1
.= dom ddbk1 /\ dom ddbk1 by FINSEQ_1:def 3
.= dom ddbk1;
k in dom dbr by A65,A12,A69,FINSEQ_3:25;
then dbrk in rng dbr by FUNCT_1:def 3;
then
A75: dbrk is Element of (3-tuples_on Bags n)*;
set vdbrk = v*(dbr.k);
A76: dom ddbk1 = Seg len ddbk1 by FINSEQ_1:def 3;
reconsider dbrk as FinSequence of 3-tuples_on Bags n by A75;
rng dbrk c= 3-tuples_on Bags n;
then
A77: dom vdbrk = dom dbrk by A27,RELAT_1:27;
then
A78: dom vdbrk = Seg len ddbk1 by A74,FINSEQ_1:def 3;
A79: dom rs = dom f by A65,A12,A68,A67,FINSEQ_3:29;
then
A80: rs/.k = rs.k by A70,PARTFUN1:def 6;
consider b1,b2 being bag of n such that
A81: db/.k = <*b1,b2*> and
A82: rs/.k = p.b1*qr.b2 by A66,A79,A70;
reconsider b19 = b1 as Element of Bags n by PRE_POLY:def 12;
consider qrs being FinSequence of the carrier of L such that
A83: qr.b2 = Sum qrs and
A84: len qrs = len decomp b2 and
A85: for i being Element of NAT st i in dom qrs ex b11, b12 being
bag of n st (decomp b2)/.i = <*b11, b12*> & qrs/.i = q.b11*r.b12 by Def10;
A86: dom qrs = dom (p.b1*qrs) by Def1;
then
A87: len qrs = len (p.b1*qrs) by FINSEQ_3:29;
A88: len <*b1,b2*> = 2 by FINSEQ_1:44;
then 1 in dom <*b1,b2*> by FINSEQ_3:25;
then
A89: dbk2 = <*b1,b2*>.1 by A81,PARTFUN1:def 6
.= b1;
reconsider vdbrk as FinSequence by A78,FINSEQ_1:def 2;
A90: Sum (p.b1*qrs) = p.b1*(Sum qrs) by Th12;
2 in dom <*b1,b2*> by A88,FINSEQ_3:25;
then
A91: (db/.k)/.2 = <*b1,b2*>.2 by A81,PARTFUN1:def 6
.= b2;
then
A92: dom vdbrk = dom (p.b1*qrs) by A84,A74,A77,A86,FINSEQ_3:29;
A93: now
let i be Nat;
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
assume
A94: 1 <= i & i <= len (p.b1*qrs);
then
A95: i in dom qrs by A86,FINSEQ_3:25;
A96: i in dom dbrk by A84,A91,A74,A87,A94,FINSEQ_3:25;
then consider b11, b12 being bag of n such that
A97: (decomp b2)/.i = <*b11, b12*> and
A98: qrs/.i = q.b11*r.b12 by A85,A77,A86,A92;
((len ddbk1) |-> <*dbk2*>).i9 = <*dbk2*> & (decomp b2)/.i = (
decomp b2).i by A91,A74,A76,A96,FUNCOP_1:7,PARTFUN1:def 6;
then
A99: dbrk.i = <*b1*>^<*b11,b12*> by A89,A91,A73,A96,A97,PRE_POLY:def 4
.= <*b1,b11,b12*> by FINSEQ_1:43;
reconsider b119 = b11, b129 = b12 as Element of Bags n
by PRE_POLY:def 12;
reconsider B = <*b19,b119,b129*> as Element of 3-tuples_on Bags n by
FINSEQ_2:104;
thus (v*(dbr.k)).i = v.(dbrk.i) by A77,A96,FUNCT_1:12
.= p.(B/.1)*q.(B/.2)*r.(B/.3) by A11,A99
.= p.b1*q.(B/.2)*r.(B/.3) by FINSEQ_4:18
.= p.b1*q.b11*r.(B/.3) by FINSEQ_4:18
.= p.b1*q.b11*r.b12 by FINSEQ_4:18
.= p.b1*(qrs/.i) by A98,GROUP_1:def 3
.= (p.b1*qrs)/.i by A95,Def1
.= (p.b1*qrs).i by A86,A95,PARTFUN1:def 6;
end;
len vdbrk = len (p.b1*qrs) by A84,A91,A74,A77,A87,FINSEQ_3:29;
then
A100: vdbrk = p.b1*qrs by A93,FINSEQ_1:14;
vdbr/.k = vdbr.k by A72,PARTFUN1:def 6
.= ((dom dbr --> v).k)*(dbr.k) by A61,A72,PBOOLE:def 19
.= p.b1*qrs by A67,A72,A100,FUNCOP_1:7;
hence (Sum vdbr).k = rs.k by A70,A82,A83,A90,A80,A71,MATRLIN:def 6;
end;
then
A101: Sum vdbr = rs by FINSEQ_1:14;
dom dbl = dom db by A1,FINSEQ_3:29;
then consider P being Permutation of dom fdbl such that
A102: fdbr = fdbl*P by A2,A13,A24,PRE_POLY:74;
rng fdbl c= 3-tuples_on Bags n;
then dom vfdbl = dom fdbl by A27,RELAT_1:27;
then reconsider P as Permutation of dom (vfdbl);
A103: vfdbr = vfdbl*P by A102,RELAT_1:36;
Sum vfdbl = Sum Sum vdbl by A26,Th14;
hence pqra.b = pqrb.b by A21,A64,A60,A63,A101,A103,RLVECT_2:7;
end;
hence thesis;
end;
definition
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable commutative non empty doubleLoopStr, p, q be Series of n
, L;
redefine func p*'q; :: redefines *' (POLYNOM1, definition)
commutativity
proof
let p, q be Series of n, L;
reconsider pq = p*'q, qp = q*'p as Function of Bags n, the carrier of L;
now
let b be Element of Bags n;
defpred P[object, object] means
ex b1, b2 being bag of n st (decomp b).$1 = <*
b1, b2*> & (decomp b).$2 = <*b2, b1*>;
consider s being FinSequence of the carrier of L such that
A1: pq.b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of
n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by Def10;
A4: dom s = dom decomp b by A2,FINSEQ_3:29;
then reconsider ds = dom s as non empty set;
A5: now
let e be object;
assume
A6: e in ds;
then consider b1, b2 being bag of n such that
A7: (decomp b)/.e = <*b1, b2*> and
A8: b = b1+b2 by A4,PRE_POLY:68;
consider d being Element of NAT such that
A9: d in dom decomp b and
A10: (decomp b)/.d = <*b2,b1*> by A8,PRE_POLY:69;
reconsider d as object;
take d;
thus d in ds by A2,A9,FINSEQ_3:29;
thus P[e,d]
proof
take b1, b2;
thus thesis by A4,A6,A7,A9,A10,PARTFUN1:def 6;
end;
end;
consider f being Function of ds, ds such that
A11: for e being object st e in ds holds P[e,f.e] from FUNCT_2:sch 1(
A5);
A12: dom f = ds by FUNCT_2:def 1;
ds c= rng f
proof
let x be object;
assume
A13: x in ds;
then consider b1, b2 being bag of n such that
A14: (decomp b).x = <*b1, b2*> and
A15: (decomp b).(f.x) = <*b2, b1*> by A11;
A16: f.x in rng f by A12,A13,FUNCT_1:def 3;
then
A17: f.(f.x) in rng f by A12,FUNCT_1:def 3;
consider b3, b4 being bag of n such that
A18: (decomp b).(f.x) = <*b3, b4*> and
A19: (decomp b).(f.(f.x)) = <*b4, b3*> by A11,A16;
b3 = b2 & b4 = b1 by A15,A18,FINSEQ_1:77;
hence thesis by A4,A13,A17,A14,A19,FUNCT_1:def 4;
end;
then
A20: rng f = ds;
f is one-to-one
proof
let x1, x2 be object such that
A21: x1 in dom f and
A22: x2 in dom f and
A23: f.x1 = f.x2;
consider b3, b4 being bag of n such that
A24: (decomp b).x2 = <*b3, b4*> and
A25: (decomp b).(f.x2) = <*b4, b3*> by A11,A22;
consider b1, b2 being bag of n such that
A26: (decomp b).x1 = <*b1, b2*> and
A27: (decomp b).(f.x1) = <*b2, b1*> by A11,A21;
b2 = b4 & b1 = b3 by A23,A27,A25,FINSEQ_1:77;
hence thesis by A4,A21,A22,A26,A24,FUNCT_1:def 4;
end;
then reconsider f as Permutation of dom s by A20,FUNCT_2:57;
consider t being FinSequence of the carrier of L such that
A28: qp.b = Sum t and
A29: len t = len decomp b and
A30: for k being Element of NAT st k in dom t ex b1, b2 being bag of
n st (decomp b)/.k = <*b1, b2*> & t/.k = q.b1*p.b2 by Def10;
A31: dom t = dom decomp b by A29,FINSEQ_3:29;
now
let i be Nat;
reconsider fi = f.i as Element of NAT;
A32: dom s = dom decomp b by A2,FINSEQ_3:29;
assume
A33: i in dom t;
then consider b1, b2 being bag of n such that
A34: (decomp b)/.i = <*b1, b2*> and
A35: t/.i = q.b1*p.b2 by A30;
A36: t/.i = t.i by A33,PARTFUN1:def 6;
consider b5, b6 being bag of n such that
A37: (decomp b).i = <*b5, b6*> and
A38: (decomp b).(f.i) = <*b6, b5*> by A4,A31,A11,A33;
dom s = dom t by A2,A29,FINSEQ_3:29;
then (decomp b)/.i = (decomp b).i by A33,A32,PARTFUN1:def 6;
then
A39: b1 = b5 & b2 = b6 by A34,A37,FINSEQ_1:77;
A40: f.i in rng f by A4,A31,A12,A33,FUNCT_1:def 3;
then
A41: s/.fi = s.fi by PARTFUN1:def 6;
consider b3, b4 being bag of n such that
A42: (decomp b)/.fi = <*b3, b4*> and
A43: s/.fi = p.b3*q.b4 by A3,A40;
A44: (decomp b)/.fi = (decomp b).fi by A40,A32,PARTFUN1:def 6;
then b3 = b6 by A42,A38,FINSEQ_1:77;
hence t.i = s.(f.i) by A35,A42,A43,A38,A36,A41,A44,A39,FINSEQ_1:77;
end;
hence pq.b = qp.b by A1,A2,A28,A29,RLVECT_2:6;
end;
hence p*'q = q*'p;
end;
end;
theorem
for n being Ordinal, L being add-associative right_complementable
right_zeroed right_unital distributive non empty doubleLoopStr, p being
Series of n, L holds p*'0_(n,L) = 0_(n,L)
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
right_unital distributive non empty doubleLoopStr, p be Series of n, L;
set Z = 0_(n,L);
now
let b be Element of Bags n;
consider s being FinSequence of the carrier of L such that
A1: (p*'Z).b = Sum s and
len s = len decomp b and
A2: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*Z.b2 by Def10;
now
let k be Nat;
assume k in dom s;
then consider b1, b2 being bag of n such that
(decomp b)/.k = <*b1, b2*> and
A3: s/.k = p.b1*Z.b2 by A2;
thus s/.k = p.b1*0.L by A3,Th22
.= 0.L;
end;
then Sum s = 0.L by MATRLIN:11;
hence (p*'Z).b = Z.b by A1;
end;
hence thesis;
end;
theorem Th29:
for n being Ordinal, L being add-associative
right_complementable right_zeroed distributive right_unital non trivial non
empty doubleLoopStr, p being Series of n, L holds p*'1_(n,L) = p
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
distributive right_unital non trivial doubleLoopStr, p be Series of
n, L;
set O = 1_(n,L), cL = the carrier of L;
now
let b be Element of Bags n;
consider s being FinSequence of cL such that
A1: (p*'O).b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*O.b2 by Def10;
consider t being FinSequence of cL, s1 being Element of cL such that
A4: s = t^<*s1*> by A2,FINSEQ_2:19;
A5: now
per cases;
suppose
t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:43;
end;
suppose
A6: t <> <*>(cL);
now
let k be Nat;
A7: len s = len t + len <*s1*> by A4,FINSEQ_1:22
.= len t +1 by FINSEQ_1:39;
assume
A8: k in dom t;
then
A9: t/.k = t.k by PARTFUN1:def 6
.= s.k by A4,A8,FINSEQ_1:def 7;
k <= len t by A8,FINSEQ_3:25;
then
A10: k < len s by A7,NAT_1:13;
A11: 1 <= k by A8,FINSEQ_3:25;
then
A12: k in dom decomp b by A2,A10,FINSEQ_3:25;
A13: dom s = dom decomp b by A2,FINSEQ_3:29;
then
A14: s/.k = s.k by A12,PARTFUN1:def 6;
per cases by A11,XXREAL_0:1;
suppose
A15: 1 < k;
consider b1, b2 being bag of n such that
A16: (decomp b)/.k = <*b1, b2*> and
A17: s/.k = p.b1*O.b2 by A3,A13,A12;
b2 <> EmptyBag n by A2,A10,A15,A16,PRE_POLY:72;
hence t/.k = p.b1*0.L by A9,A14,A17,Th25
.= 0.L;
end;
suppose
A18: k = 1;
A19: now
assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73;
then len t +1 = 0 qua Nat+1 by A2,A7,FINSEQ_1:39;
hence contradiction by A6;
end;
consider b1, b2 being bag of n such that
A20: (decomp b)/.k = <*b1, b2*> and
A21: s/.k = p.b1*O.b2 by A3,A13,A12;
(decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71;
then b1 = EmptyBag n & b2 = b by A18,A20,FINSEQ_1:77;
then s.k = (p.EmptyBag n)*0.L by A14,A21,A19,Th25
.= 0.L;
hence t/.k = 0.L by A9;
end;
end;
hence (Sum t) = 0.L by MATRLIN:11;
end;
end;
A22: s.len s = (t^<*s1*>).(len t +1) by A4,FINSEQ_2:16
.= s1 by FINSEQ_1:42;
A23: Sum s = (Sum t) + (Sum <*s1*>) by A4,RLVECT_1:41;
s is non empty by A2;
then
A24: len s in dom s by FINSEQ_5:6;
then consider b1, b2 being bag of n such that
A25: (decomp b)/.len s = <*b1, b2*> and
A26: s/.len s = p.b1*O.b2 by A3;
A27: s/.len s = s.len s by A24,PARTFUN1:def 6;
(decomp b)/.len s = <*b, EmptyBag n*> by A2,PRE_POLY:71;
then
A28: b1 = b & b2 = EmptyBag n by A25,FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= p.b*1.L by A26,A28,A22,A27,Th25
.= p.b;
hence (p*'O).b = p.b by A1,A23,A5,RLVECT_1:4;
end;
hence thesis;
end;
theorem Th30:
for n being Ordinal, L being add-associative
right_complementable right_zeroed distributive well-unital non trivial non
empty doubleLoopStr, p being Series of n, L holds 1_(n,L)*'p = p
proof
let n be Ordinal, L be add-associative right_complementable right_zeroed
distributive well-unital non trivial doubleLoopStr, p be Series of
n, L;
set O = 1_(n,L), cL = the carrier of L;
now
let b be Element of Bags n;
consider s being FinSequence of cL such that
A1: (O*'p).b = Sum s and
A2: len s = len decomp b and
A3: for k being Element of NAT st k in dom s ex b1, b2 being bag of n
st (decomp b)/.k = <*b1, b2*> & s/.k = O.b1*p.b2 by Def10;
s is non empty by A2;
then consider s1 being Element of cL, t being FinSequence of cL such that
A4: s1 = s.1 and
A5: s = <*s1*>^t by FINSEQ_3:102;
A6: Sum s = (Sum <*s1*>) + (Sum t) by A5,RLVECT_1:41;
A7: now
per cases;
suppose
t = <*>(cL);
hence (Sum t) = 0.L by RLVECT_1:43;
end;
suppose
A8: t <> <*>(cL);
now
let k be Nat;
A9: len s = len t + len <*s1*> by A5,FINSEQ_1:22
.= len t +1 by FINSEQ_1:39;
assume
A10: k in dom t;
then
A11: t/.k = t.k by PARTFUN1:def 6
.= s.(k+1) by A5,A10,FINSEQ_3:103;
1 <= k by A10,FINSEQ_3:25;
then
A12: 1 < k+1 by NAT_1:13;
k <= len t by A10,FINSEQ_3:25;
then
A13: k+1 <= len s by A9,XREAL_1:6;
then
A14: k+1 in dom decomp b by A2,A12,FINSEQ_3:25;
A15: dom s = dom decomp b by A2,FINSEQ_3:29;
then
A16: s/.(k+1) = s.(k+1) by A14,PARTFUN1:def 6;
per cases by A13,XXREAL_0:1;
suppose
A17: k+1 < len s;
consider b1, b2 being bag of n such that
A18: (decomp b)/.(k+1) = <*b1, b2*> and
A19: s/.(k+1) = O.b1*p.b2 by A3,A15,A14;
b1 <> EmptyBag n by A2,A12,A17,A18,PRE_POLY:72;
hence t/.k = 0.L*p.b2 by A11,A16,A19,Th25
.= 0.L;
end;
suppose
A20: k+1 = len s;
A21: now
assume b = EmptyBag n;
then decomp b = <* <*EmptyBag n, EmptyBag n*> *> by PRE_POLY:73;
then len t +1 = 0 qua Nat+1 by A2,A9,FINSEQ_1:39;
hence contradiction by A8;
end;
consider b1, b2 being bag of n such that
A22: (decomp b)/.(k+1) = <*b1, b2*> and
A23: s/.(k+1) = O.b1*p.b2 by A3,A15,A14;
(decomp b)/.len s = <*b,EmptyBag n*> by A2,PRE_POLY:71;
then b2 = EmptyBag n & b1 = b by A20,A22,FINSEQ_1:77;
then s.(k+1) = 0.L*(p.EmptyBag n) by A16,A23,A21,Th25
.= 0.L;
hence t/.k = 0.L by A11;
end;
end;
hence Sum t = 0.L by MATRLIN:11;
end;
end;
A24: s is non empty by A2;
then consider b1, b2 being bag of n such that
A25: (decomp b)/.1 = <*b1, b2*> and
A26: s/.1 = O.b1*p.b2 by A3,FINSEQ_5:6;
1 in dom s by A24,FINSEQ_5:6;
then
A27: s/.1 = s.1 by PARTFUN1:def 6;
(decomp b)/.1 = <*EmptyBag n, b*> by PRE_POLY:71;
then
A28: b2 = b & b1 = EmptyBag n by A25,FINSEQ_1:77;
Sum <*s1*> = s1 by RLVECT_1:44
.= 1.L*p.b by A4,A26,A28,A27,Th25
.= p.b;
hence (O*'p).b = p.b by A1,A6,A7,RLVECT_1:4;
end;
hence thesis;
end;
begin :: Polynomials ----------------------------------------------------------
registration
let n be set, S be non empty ZeroStr;
cluster finite-Support for Series of n, S;
existence
proof
reconsider P = Bags n --> 0.S as Function of Bags n, the carrier of S;
reconsider P as Function of Bags n, S;
reconsider P as Series of n, S;
take P;
for x being Element of Bags n holds x in {} iff P.x <> 0.S;
then Support P = {}Bags n by Def4;
hence Support P is finite;
end;
end;
definition
let n be Ordinal, S be non empty ZeroStr;
mode Polynomial of n, S is finite-Support Series of n, S;
end;
registration
let n be Ordinal, L be right_zeroed non empty addLoopStr, p, q be
Polynomial of n, L;
cluster p+q -> finite-Support;
coherence
proof
set Sp = Support p, Sq = Support q;
Support p is finite & Support q is finite by Def5;
then Sp \/ Sq is finite;
then Support (p+q) is finite by Th20,FINSET_1:1;
hence thesis;
end;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p be Polynomial of n, L;
cluster -p -> finite-Support;
coherence
proof
set f = -p;
A1: Support f c= Support p
proof
let x be object;
assume
A2: x in Support f;
then reconsider x9 = x as Element of Bags n;
f.x9 <> 0.L by A2,Def4;
then -(p.x9) <> 0.L by Th17;
then p.x9 <> 0.L by RLVECT_1:12;
hence thesis by Def4;
end;
Support p is finite by Def5;
hence thesis by A1;
end;
end;
registration
let n be Element of NAT, L be add-associative right_zeroed
right_complementable non empty addLoopStr, p, q be Polynomial of n, L;
cluster p-q -> finite-Support;
coherence;
end;
registration
let n be Ordinal, S be non empty ZeroStr;
cluster 0_(n, S) -> finite-Support;
coherence
proof
set Z = 0_(n, S);
now
given x being object such that
A1: x in Support Z;
reconsider x as Element of Bags n by A1;
Z.x = 0.S;
hence contradiction by A1,Def4;
end;
then Support Z = {} by XBOOLE_0:def 1;
hence thesis;
end;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
right_unital right-distributive non trivial doubleLoopStr;
cluster 1_(n,L) -> finite-Support;
coherence
proof
reconsider O = 0_(n,L)+*(EmptyBag n,1.L) as Function of Bags n, the
carrier of L;
reconsider O9 = O as Function of Bags n, L;
reconsider O9 as Series of n, L;
now
let x be object;
hereby
assume
A1: x in Support O9;
then reconsider x9 = x as Element of Bags n;
assume x <> EmptyBag n;
then O9.x = 0_(n,L).x9 by FUNCT_7:32
.= 0.L;
hence contradiction by A1,Def4;
end;
assume
A2: x = EmptyBag n;
dom 0_(n,L) = Bags n;
then O9.x <> 0.L by A2,FUNCT_7:31;
hence x in Support O9 by A2,Def4;
end;
then Support O9 = {EmptyBag n} by TARSKI:def 1;
hence thesis;
end;
end;
registration
let n be Ordinal, L be add-associative right_complementable right_zeroed
right_unital distributive non empty doubleLoopStr, p, q be Polynomial of n, L;
cluster p*'q -> finite-Support;
coherence
proof
deffunc F(Element of Bags n,Element of Bags n) = $1+$2;
set D = { F(b1,b2) where b1, b2 is Element of Bags n : b1 in Support p &
b2 in Support q };
A1: Support q is finite by Def5;
A2: Support (p*'q) c= D
proof
let x9 be object;
assume
A3: x9 in Support (p*'q);
then reconsider b = x9 as Element of Bags n;
consider s being FinSequence of the carrier of L such that
A4: (p*'q).b = Sum s and
A5: len s = len decomp b and
A6: for k being Element of NAT st k in dom s ex b1, b2 being bag of
n st (decomp b)/.k = <*b1, b2*> & s/.k = p.b1*q.b2 by Def10;
(p*'q).b <> 0.L by A3,Def4;
then consider k being Nat such that
A7: k in dom s and
A8: s/.k <> 0.L by A4,MATRLIN:11;
consider b1, b2 being bag of n such that
A9: (decomp b)/.k = <*b1, b2*> and
A10: s/.k = p.b1*q.b2 by A6,A7;
A11: b1 in Bags n by PRE_POLY:def 12;
A12: b2 in Bags n by PRE_POLY:def 12;
q.b2 <> 0.L by A8,A10;
then
A13: b2 in Support q by A12,Def4;
p.b1 <> 0.L by A8,A10;
then
A14: b1 in Support p by A11,Def4;
k in dom decomp b by A5,A7,FINSEQ_3:29;
then consider b19, b29 being bag of n such that
A15: (decomp b)/.k = <*b19, b29*> and
A16: b = b19+b29 by PRE_POLY:68;
b19 = b1 & b29 = b2 by A9,A15,FINSEQ_1:77;
hence thesis by A14,A13,A16;
end;
A17: Support p is finite by Def5;
D is finite from FRAENKEL:sch 22(A17, A1);
hence thesis by A2;
end;
end;
begin :: The ring of polynomials ---------------------------------------------
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
right_unital distributive non trivial doubleLoopStr;
func Polynom-Ring (n, L) -> strict non empty doubleLoopStr means
:Def11:
(
for x being set holds x in the carrier of it iff x is Polynomial of n, L) & (
for x, y being Element of it, p, q being Polynomial of n, L st x = p & y = q
holds x+y = p+q) & (for x, y being Element of it, p, q being Polynomial of n, L
st x = p & y = q holds x*y = p*'q) & 0.it = 0_(n,L) & 1.it = 1_(n,L);
existence
proof
reconsider Z = (Bags n) --> 0.L as Function of Bags n, the carrier of L;
defpred M[set, set, set] means ex p, q, r being Polynomial of n, L st p =
$1 & q = $2 & r = $3 & p*'q=r;
defpred A[set, set, set] means ex p, q, r being Polynomial of n, L st p =
$1 & q = $2 & r = $3 & p+q=r;
set x9 = the finite-Support Series of n, L;
defpred Q[set] means ex x9 being Series of n, L st x9 = $1 & x9 is
finite-Support;
consider P being Subset of Funcs(Bags n, the carrier of L) such that
A1: for x being Element of Funcs(Bags n, the carrier of L)holds x in P
iff Q[x] from SUBSET_1:sch 3;
x9 in Funcs(Bags n, the carrier of L) by FUNCT_2:8;
then reconsider
P as non empty Subset of Funcs(Bags n, the carrier of L) by A1;
A2: now
let x be Element of P, y be Element of P;
reconsider p = x, q = y as Element of Funcs(Bags n, the carrier of L);
consider p9 being Series of n, L such that
A3: p9 = p and
A4: p9 is finite-Support by A1;
consider q9 being Series of n, L such that
A5: q9 = q and
A6: q9 is finite-Support by A1;
reconsider p9, q9 as Polynomial of n, L by A4,A6;
set r = p9+q9;
r in Funcs(Bags n, the carrier of L) by FUNCT_2:8;
then reconsider u = r as Element of P by A1;
take u;
thus A[x,y,u] by A3,A5;
end;
consider fadd being Function of [:P,P:],P such that
A7: for x being Element of P, y being Element of P holds A[x,y,fadd.(x
,y)] from BINOP_1:sch 3(A2);
A8: now
let x be Element of P, y be Element of P;
reconsider p = x, q = y as Element of Funcs(Bags n, the carrier of L);
consider p9 being Series of n, L such that
A9: p9 = p and
A10: p9 is finite-Support by A1;
consider q9 being Series of n, L such that
A11: q9 = q and
A12: q9 is finite-Support by A1;
reconsider p9, q9 as Polynomial of n, L by A10,A12;
set r = p9*'q9;
r in Funcs(Bags n, the carrier of L) by FUNCT_2:8;
then reconsider u = r as Element of P by A1;
take u;
thus M[x,y,u] by A9,A11;
end;
consider fmult being Function of [:P,P:],P such that
A13: for x being Element of P, y being Element of P holds M[x,y,fmult.
(x,y)] from BINOP_1:sch 3(A8);
reconsider ZZ = Z as Element of Funcs(Bags n, the carrier of L) by
FUNCT_2:8;
reconsider Z9 = Z as Function of Bags n, L;
reconsider Z9 as Series of n, L;
now
given x being object such that
A14: x in Support Z9;
reconsider x as Element of Bags n by A14;
Z9.x = 0.L;
hence contradiction by A14,Def4;
end;
then Support Z9 = {} by XBOOLE_0:def 1;
then Z9 is finite-Support;
then ZZ in P by A1;
then reconsider Ze = Z as Element of P;
reconsider O = Z+*(EmptyBag n,1.L) as Function of Bags n, the carrier of L;
reconsider O9 = O as Function of Bags n, L;
reconsider O9 as Series of n, L;
reconsider O as Element of Funcs(Bags n, the carrier of L) by FUNCT_2:8;
now
let x be object;
hereby
assume
A15: x in Support O9;
then reconsider x9 = x as Element of Bags n;
assume x <> EmptyBag n;
then O9.x = Z.x9 by FUNCT_7:32
.= 0.L;
hence contradiction by A15,Def4;
end;
assume
A16: x = EmptyBag n;
dom Z = Bags n;
then O9.x <> 0.L by A16,FUNCT_7:31;
hence x in Support O9 by A16,Def4;
end;
then Support O9 = {EmptyBag n} by TARSKI:def 1;
then O9 is finite-Support;
then reconsider O as Element of P by A1;
reconsider R = doubleLoopStr(# P, fadd, fmult, O, Ze #) as strict non
empty doubleLoopStr;
take R;
thus for x being set holds x in the carrier of R iff x is Polynomial of n,
L
proof
let x be set;
hereby
assume
A17: x in the carrier of R;
then reconsider xx = x as Element of Funcs(Bags n, the carrier of L);
ex x9 being Series of n, L st x9 = xx & x9 is finite-Support by A1,A17;
hence x is Polynomial of n, L;
end;
assume
A18: x is Polynomial of n, L;
then x is Element of Funcs(Bags n, the carrier of L) by FUNCT_2:8;
hence thesis by A1,A18;
end;
hereby
let x, y be Element of R, p, q be Polynomial of n, L such that
A19: x = p & y = q;
ex p9, q9, r9 being Polynomial of n, L st p9 = x & q9 = y & r9 =
fadd.(x,y) & p9+q9= r9 by A7;
hence x+y = p+q by A19;
end;
hereby
let x, y be Element of R, p, q be Polynomial of n, L such that
A20: x = p & y = q;
ex p9, q9, r9 being Polynomial of n, L st p9 = x & q9 = y & r9 =
fmult.(x,y) & p9*'q9= r9 by A13;
hence x*y = p*'q by A20;
end;
thus 0.R = 0_(n,L);
thus thesis;
end;
uniqueness
proof
let it1, it2 be strict non empty doubleLoopStr such that
A21: for x being set holds x in the carrier of it1 iff x is Polynomial
of n, L and
A22: for x, y being Element of it1, p, q being Polynomial of n, L st x
= p & y = q holds x+y = p+q and
A23: for x, y being Element of it1, p, q being Polynomial of n, L st x
= p & y = q holds x*y = p*'q and
A24: 0.it1 = 0_(n,L) & 1.it1 = 1_(n,L) and
A25: for x being set holds x in the carrier of it2 iff x is Polynomial
of n, L and
A26: for x, y being Element of it2, p, q being Polynomial of n, L st x
= p & y = q holds x+y = p+q and
A27: for x, y being Element of it2, p, q being Polynomial of n, L st x
= p & y = q holds x*y = p*'q and
A28: 0.it2 = 0_(n,L) & 1.it2 = 1_(n,L);
A29: now
let x be object;
hereby
assume x in the carrier of it1;
then x is Polynomial of n, L by A21;
hence x in the carrier of it2 by A25;
end;
assume x in the carrier of it2;
then x is Polynomial of n, L by A25;
hence x in the carrier of it1 by A21;
end;
then
A30: the carrier of it1 = the carrier of it2 by TARSKI:2;
A31: now
let a, b be Element of it1;
reconsider a9 = a, b9 = b as Element of it2 by A29;
reconsider a19 = a9, b19 = b9 as Element of it2;
reconsider p = a, q = b as Polynomial of n, L by A21;
reconsider a1 = a, b1 = b as Element of it1;
thus (the multF of it1).(a, b) = a1*b1 .= p*'q by A23
.= a19*b19 by A27
.= (the multF of it2).(a, b);
end;
now
let a, b be Element of it1;
reconsider a9 = a, b9 = b as Element of it2 by A29;
reconsider a19 = a9, b19 = b9 as Element of it2;
reconsider p = a, q = b as Polynomial of n, L by A21;
reconsider a1 = a, b1 = b as Element of it1;
thus (the addF of it1).(a, b) = a1+b1 .= p+q by A22
.= a19+b19 by A26
.= (the addF of it2).(a, b);
end;
then the addF of it1 = the addF of it2 by A30,BINOP_1:2;
hence thesis by A24,A28,A30,A31,BINOP_1:2;
end;
end;
registration
let n be Ordinal, L be Abelian right_zeroed add-associative
right_complementable right_unital distributive non trivial
doubleLoopStr;
cluster Polynom-Ring (n, L) -> Abelian;
coherence
proof
set Pm = Polynom-Ring (n, L);
let v, w be Element of Pm;
reconsider p = v, q = w as Polynomial of n, L by Def11;
thus v + w = q+p by Def11
.= w + v by Def11;
end;
end;
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> add-associative;
coherence
proof
set Pm = Polynom-Ring (n, L);
let u, v, w be Element of Pm;
reconsider o = u, p = v, q = w as Polynomial of n, L by Def11;
A1: v+w = p+q by Def11;
u+v = o+p by Def11;
hence (u+v)+w = (o+p)+q by Def11
.= o+(p+q) by Th21
.= u+(v+w) by A1,Def11;
end;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> right_zeroed;
coherence
proof
let v be Element of Polynom-Ring (n, L);
reconsider p = v as Polynomial of n, L by Def11;
0.Polynom-Ring (n, L) = 0_(n,L) by Def11;
hence v + 0.Polynom-Ring (n, L) = p+0_(n,L) by Def11
.= v by Th23;
end;
end;
registration
let n be Ordinal, L be right_complementable right_zeroed add-associative
right_unital distributive non trivial doubleLoopStr;
cluster Polynom-Ring (n, L) -> right_complementable;
coherence
proof
let v be Element of Polynom-Ring (n,L);
reconsider p = v as Polynomial of n, L by Def11;
reconsider w = -p as Element of Polynom-Ring(n,L) by Def11;
take w;
thus v + w = p-p by Def11
.= 0_(n,L) by Th24
.= 0.Polynom-Ring(n,L) by Def11;
end;
end;
registration
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable commutative right_unital distributive non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> commutative;
coherence
proof
set Pm = Polynom-Ring (n, L);
let v, w be Element of Pm;
reconsider p = v, q = w as Polynomial of n, L by Def11;
thus v*w = q*'p by Def11
.= w*v by Def11;
end;
end;
registration
let n be Ordinal, L be Abelian add-associative right_zeroed
right_complementable right_unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> associative;
coherence
proof
set Pm = Polynom-Ring (n, L);
let x,y,z be Element of Pm;
reconsider p = x, q = y, r = z as Polynomial of n, L by Def11;
A1: y*z = q*'r by Def11;
x*y = p*'q by Def11;
hence (x*y)*z = (p*'q)*'r by Def11
.= p*'(q*'r) by Th27
.= x*(y*z) by A1,Def11;
end;
end;
Lm1: now
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr;
set Pm = Polynom-Ring (n, L);
let x, e be Element of Pm;
reconsider p = x as Polynomial of n, L by Def11;
assume
A1: e = 1.Pm;
A2: 1.Pm = 1_(n,L) by Def11;
hence x*e = p*'1_(n,L) by A1,Def11
.= x by Th29;
thus e*x = 1_(n,L)*'p by A1,A2,Def11
.= x by Th30;
end;
registration
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> well-unital right-distributive;
coherence
proof
set Pm = Polynom-Ring (n, L);
thus Pm is well-unital
by Lm1;
let x, y, z be Element of Pm;
reconsider p = x, q = y, r = z as Polynomial of n, L by Def11;
A1: x*y = p*'q & x*z = p*'r by Def11;
y+z = q+r by Def11;
hence x*(y+z) = p*'(q+r) by Def11
.= p*'q+p*'r by Th26
.= x*y + x*z by A1,Def11;
end;
end;
theorem
for n being Ordinal, L being right_zeroed Abelian add-associative
right_complementable right_unital distributive associative non trivial non
empty doubleLoopStr holds 1.Polynom-Ring(n, L) = 1_(n,L) by Def11;