:: POLYNOM1 semantic presentation
begin
registration
cluster non empty degenerated right_complementable right-distributive right_unital add-associative right_zeroed -> non empty trivial right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st b1 is degenerated holds
b1 is trivial
proof
let L be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is degenerated implies L is trivial )
assume A1: 0. L = 1. L ; :: according to STRUCT_0:def_8 ::_thesis: L is trivial
let u be Element of L; :: according to STRUCT_0:def_18 ::_thesis: u = 0. L
thus u = u * (1. L) by VECTSP_1:def_4
.= 0. L by A1, VECTSP_1:6 ; ::_thesis: verum
end;
end;
registration
cluster non empty non trivial right_complementable right-distributive right_unital add-associative right_zeroed -> non empty non degenerated right_complementable right-distributive right_unital add-associative right_zeroed for doubleLoopStr ;
coherence
for b1 being non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr st not b1 is trivial holds
not b1 is degenerated ;
end;
theorem Th1: :: POLYNOM1:1
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1
proof
let K be non empty addLoopStr ; ::_thesis: for p1, p2 being FinSequence of the carrier of K st dom p1 = dom p2 holds
dom (p1 + p2) = dom p1
let p1, p2 be FinSequence of the carrier of K; ::_thesis: ( dom p1 = dom p2 implies dom (p1 + p2) = dom p1 )
assume A1: dom p1 = dom p2 ; ::_thesis: dom (p1 + p2) = dom p1
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 ; ::_thesis: verum
end;
theorem Th2: :: POLYNOM1:2
for L being non empty addLoopStr
for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F
proof
let L be non empty addLoopStr ; ::_thesis: for F being FinSequence of the carrier of L * holds dom (Sum F) = dom F
let F be FinSequence of the carrier of L * ; ::_thesis: dom (Sum F) = dom F
len (Sum F) = len F by MATRLIN:def_6;
hence dom (Sum F) = dom F by FINSEQ_3:29; ::_thesis: verum
end;
theorem Th3: :: POLYNOM1:3
for L being non empty addLoopStr
for 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 ; ::_thesis: for F being FinSequence of the carrier of L * holds Sum (<*> ( the carrier of L *)) = <*> the carrier of L
let F be FinSequence of the carrier of L * ; ::_thesis: Sum (<*> ( the carrier of L *)) = <*> the carrier of L
dom (Sum (<*> ( the carrier of L *))) = dom (<*> ( the carrier of L *)) by Th2;
hence Sum (<*> ( the carrier of L *)) = <*> the carrier of L ; ::_thesis: verum
end;
theorem Th4: :: POLYNOM1:4
for L being non empty addLoopStr
for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>
proof
let L be non empty addLoopStr ; ::_thesis: for p being Element of the carrier of L * holds <*(Sum p)*> = Sum <*p*>
let p be Element of the carrier of L * ; ::_thesis: <*(Sum p)*> = Sum <*p*>
A1: now__::_thesis:_for_i_being_Nat_st_i_in_dom_<*p*>_holds_
<*(Sum_p)*>_/._i_=_Sum_(<*p*>_/._i)
let i be Nat; ::_thesis: ( i in dom <*p*> implies <*(Sum p)*> /. i = Sum (<*p*> /. i) )
assume i in dom <*p*> ; ::_thesis: <*(Sum p)*> /. i = Sum (<*p*> /. i)
then i in {1} by FINSEQ_1:2, FINSEQ_1: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 ;
::_thesis: verum
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 <*(Sum p)*> = Sum <*p*> by A3, A1, MATRLIN:def_6; ::_thesis: verum
end;
theorem Th5: :: POLYNOM1:5
for L being non empty addLoopStr
for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)
proof
let L be non empty addLoopStr ; ::_thesis: for F, G being FinSequence of the carrier of L * holds Sum (F ^ G) = (Sum F) ^ (Sum G)
let F, G be FinSequence of the carrier of L * ; ::_thesis: Sum (F ^ G) = (Sum F) ^ (Sum G)
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__::_thesis:_for_i_being_Nat_st_i_in_dom_(F_^_G)_holds_
((Sum_F)_^_(Sum_G))_/._i_=_Sum_((F_^_G)_/._i)
let i be Nat; ::_thesis: ( i in dom (F ^ G) implies ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1) )
assume A6: i in dom (F ^ G) ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1)
percases ( i in dom F or ex n being Nat st
( n in dom G & i = (len F) + n ) ) by A6, FINSEQ_1:25;
supposeA7: i in dom F ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1)
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 ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom G & i = (len F) + n ) ; ::_thesis: ((Sum F) ^ (Sum G)) /. b1 = Sum ((F ^ G) /. b1)
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 ; ::_thesis: verum
end;
end;
end;
hence Sum (F ^ G) = (Sum F) ^ (Sum G) by A3, A4, MATRLIN:def_6; ::_thesis: verum
end;
definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
redefine func a * p means :Def1: :: POLYNOM1:def 1
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = a * (p /. i) ) );
compatibility
for b1 being FinSequence of the carrier of L holds
( b1 = a * p iff ( dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = a * (p /. i) ) ) )
proof
A1: now__::_thesis:_for_G_being_FinSequence_of_the_carrier_of_L_st_dom_G_=_dom_p_&_(_for_i_being_set_st_i_in_dom_p_holds_
G_/._i_=_a_*_(p_/._i)_)_holds_
G_=_a_*_p
set R = (a multfield) * p;
let G be FinSequence of the carrier of L; ::_thesis: ( dom G = dom p & ( for i being set st i in dom p holds
G /. i = a * (p /. i) ) implies G = a * p )
assume that
A2: dom G = dom p and
A3: for i being set st i in dom p holds
G /. i = a * (p /. i) ; ::_thesis: G = a * p
A4: for k being set st k in dom G holds
G . k = ((a multfield) * p) . k
proof
let k be set ; ::_thesis: ( k in dom G implies G . k = ((a multfield) * p) . k )
assume A5: k in dom G ; ::_thesis: G . k = ((a multfield) * p) . k
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
.= ((a multfield) * p) . k by A2, A5, FUNCT_1:13 ;
hence G . k = ((a multfield) * p) . k ; ::_thesis: verum
end;
( rng p c= the carrier of L & dom (a multfield) = the carrier of L ) by FUNCT_2:def_1;
then dom G = dom ((a multfield) * p) by A2, RELAT_1:27;
then G = (a multfield) * p by A4, FUNCT_1:2;
hence G = a * p by FVSUM_1:def_6; ::_thesis: verum
end;
set F = a * p;
A6: rng p c= dom (a multfield)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in dom (a multfield) )
dom (a multfield) = the carrier of L by FUNCT_2:def_1;
hence ( not x in rng p or x in dom (a multfield) ) ; ::_thesis: verum
end;
A7: a * p = (a multfield) * p by FVSUM_1:def_6;
then A8: dom (a * p) = dom p by A6, RELAT_1:27;
for i being set st i in dom p holds
(a * p) /. i = a * (p /. i)
proof
let i be set ; ::_thesis: ( i in dom p implies (a * p) /. i = a * (p /. i) )
assume A9: i in dom p ; ::_thesis: (a * p) /. i = a * (p /. i)
(a * p) . 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 (a * p) /. i = a * (p /. i) by A8, A9, PARTFUN1:def_6; ::_thesis: verum
end;
hence for b1 being FinSequence of the carrier of L holds
( b1 = a * p iff ( dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = a * (p /. i) ) ) ) by A7, A6, A1, RELAT_1:27; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines * POLYNOM1:def_1_:_
for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = a * p iff ( dom b4 = dom p & ( for i being set st i in dom p holds
b4 /. i = a * (p /. i) ) ) );
definition
let L be non empty multMagma ;
let p be FinSequence of the carrier of L;
let a be Element of L;
funcp * a -> FinSequence of the carrier of L means :Def2: :: POLYNOM1:def 2
( dom it = dom p & ( for i being set st i in dom p holds
it /. i = (p /. i) * a ) );
existence
ex b1 being FinSequence of the carrier of L st
( dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) )
proof
deffunc H1( set ) -> Element of the carrier of L = (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 = H1(j) from FINSEQ_4:sch_2();
take f ; ::_thesis: ( dom f = dom p & ( for i being set st i in dom p holds
f /. i = (p /. i) * a ) )
thus A3: dom f = dom p by A1, FINSEQ_3:29; ::_thesis: for i being set st i in dom p holds
f /. i = (p /. i) * a
let j be set ; ::_thesis: ( j in dom p implies f /. j = (p /. j) * a )
assume j in dom p ; ::_thesis: f /. j = (p /. j) * a
hence f /. j = (p /. j) * a by A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of the carrier of L st dom b1 = dom p & ( for i being set st i in dom p holds
b1 /. i = (p /. i) * a ) & dom b2 = dom p & ( for i being set st i in dom p holds
b2 /. i = (p /. i) * a ) holds
b1 = b2
proof
let it1, it2 be FinSequence of the carrier of L; ::_thesis: ( dom it1 = dom p & ( for i being set st i in dom p holds
it1 /. i = (p /. i) * a ) & dom it2 = dom p & ( for i being set st i in dom p holds
it2 /. i = (p /. i) * a ) implies it1 = it2 )
assume that
A4: dom it1 = dom p and
A5: for i being set st i in dom p holds
it1 /. i = (p /. i) * a and
A6: dom it2 = dom p and
A7: for i being set st i in dom p holds
it2 /. i = (p /. i) * a ; ::_thesis: it1 = it2
now__::_thesis:_for_j_being_Nat_st_j_in_dom_p_holds_
it1_/._j_=_it2_/._j
let j be Nat; ::_thesis: ( j in dom p implies it1 /. j = it2 /. j )
assume A8: j in dom p ; ::_thesis: it1 /. j = it2 /. j
hence it1 /. j = (p /. j) * a by A5
.= it2 /. j by A7, A8 ;
::_thesis: verum
end;
hence it1 = it2 by A4, A6, FINSEQ_5:12; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines * POLYNOM1:def_2_:_
for L being non empty multMagma
for p being FinSequence of the carrier of L
for a being Element of L
for b4 being FinSequence of the carrier of L holds
( b4 = p * a iff ( dom b4 = dom p & ( for i being set st i in dom p holds
b4 /. i = (p /. i) * a ) ) );
theorem Th6: :: POLYNOM1:6
for L being non empty multMagma
for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L
proof
let L be non empty multMagma ; ::_thesis: for a being Element of L holds a * (<*> the carrier of L) = <*> the carrier of L
let a be Element of L; ::_thesis: a * (<*> the carrier of L) = <*> the carrier of L
dom (a * (<*> the carrier of L)) = dom (<*> the carrier of L) by Def1;
hence a * (<*> the carrier of L) = <*> the carrier of L ; ::_thesis: verum
end;
theorem Th7: :: POLYNOM1:7
for L being non empty multMagma
for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L
proof
let L be non empty multMagma ; ::_thesis: for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L
let a be Element of L; ::_thesis: (<*> the carrier of L) * a = <*> the carrier of L
dom ((<*> the carrier of L) * a) = dom (<*> the carrier of L) by Def2;
hence (<*> the carrier of L) * a = <*> the carrier of L ; ::_thesis: verum
end;
theorem Th8: :: POLYNOM1:8
for L being non empty multMagma
for a, b being Element of L holds a * <*b*> = <*(a * b)*>
proof
let L be non empty multMagma ; ::_thesis: for a, b being Element of L holds a * <*b*> = <*(a * b)*>
let a, b be Element of L; ::_thesis: a * <*b*> = <*(a * b)*>
A1: for i being set st i in dom <*b*> holds
<*(a * b)*> /. i = a * (<*b*> /. i)
proof
let i be set ; ::_thesis: ( i in dom <*b*> implies <*(a * b)*> /. i = a * (<*b*> /. i) )
assume i in dom <*b*> ; ::_thesis: <*(a * b)*> /. i = a * (<*b*> /. i)
then i in {1} by FINSEQ_1:2, FINSEQ_1: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 ;
::_thesis: verum
end;
dom <*(a * b)*> = Seg 1 by FINSEQ_1:38
.= dom <*b*> by FINSEQ_1:38 ;
hence a * <*b*> = <*(a * b)*> by A1, Def1; ::_thesis: verum
end;
theorem Th9: :: POLYNOM1:9
for L being non empty multMagma
for a, b being Element of L holds <*b*> * a = <*(b * a)*>
proof
let L be non empty multMagma ; ::_thesis: for a, b being Element of L holds <*b*> * a = <*(b * a)*>
let a, b be Element of L; ::_thesis: <*b*> * a = <*(b * a)*>
A1: for i being set st i in dom <*b*> holds
<*(b * a)*> /. i = (<*b*> /. i) * a
proof
let i be set ; ::_thesis: ( i in dom <*b*> implies <*(b * a)*> /. i = (<*b*> /. i) * a )
assume i in dom <*b*> ; ::_thesis: <*(b * a)*> /. i = (<*b*> /. i) * a
then i in {1} by FINSEQ_1:2, FINSEQ_1: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 ;
::_thesis: verum
end;
dom <*(b * a)*> = Seg 1 by FINSEQ_1:38
.= dom <*b*> by FINSEQ_1:38 ;
hence <*b*> * a = <*(b * a)*> by A1, Def2; ::_thesis: verum
end;
theorem Th10: :: POLYNOM1:10
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)
proof
let L be non empty multMagma ; ::_thesis: for a being Element of L
for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)
let a be Element of L; ::_thesis: for p, q being FinSequence of the carrier of L holds a * (p ^ q) = (a * p) ^ (a * q)
let p, q be FinSequence of the carrier of L; ::_thesis: a * (p ^ q) = (a * p) ^ (a * q)
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__::_thesis:_for_i_being_Nat_st_i_in_dom_(a_*_(p_^_q))_holds_
(a_*_(p_^_q))_/._i_=_((a_*_p)_^_(a_*_q))_/._i
let i be Nat; ::_thesis: ( i in dom (a * (p ^ q)) implies (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1 )
assume A7: i in dom (a * (p ^ q)) ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1
percases ( i in dom p or ex n being Nat st
( n in dom q & i = (len p) + n ) ) by A1, A7, FINSEQ_1:25;
supposeA8: i in dom p ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1
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 ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom q & i = (len p) + n ) ; ::_thesis: (a * (p ^ q)) /. b1 = ((a * p) ^ (a * q)) /. b1
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 ; ::_thesis: verum
end;
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 a * (p ^ q) = (a * p) ^ (a * q) by A6, FINSEQ_5:12; ::_thesis: verum
end;
theorem Th11: :: POLYNOM1:11
for L being non empty multMagma
for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
proof
let L be non empty multMagma ; ::_thesis: for a being Element of L
for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
let a be Element of L; ::_thesis: for p, q being FinSequence of the carrier of L holds (p ^ q) * a = (p * a) ^ (q * a)
let p, q be FinSequence of the carrier of L; ::_thesis: (p ^ q) * a = (p * a) ^ (q * a)
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__::_thesis:_for_i_being_Nat_st_i_in_dom_((p_^_q)_*_a)_holds_
((p_^_q)_*_a)_/._i_=_((p_*_a)_^_(q_*_a))_/._i
let i be Nat; ::_thesis: ( i in dom ((p ^ q) * a) implies ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1 )
assume A7: i in dom ((p ^ q) * a) ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1
percases ( i in dom p or ex n being Nat st
( n in dom q & i = (len p) + n ) ) by A1, A7, FINSEQ_1:25;
supposeA8: i in dom p ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1
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 ; ::_thesis: verum
end;
suppose ex n being Nat st
( n in dom q & i = (len p) + n ) ; ::_thesis: ((p ^ q) * a) /. b1 = ((p * a) ^ (q * a)) /. b1
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 ; ::_thesis: verum
end;
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 (p ^ q) * a = (p * a) ^ (q * a) by A6, FINSEQ_5:12; ::_thesis: verum
end;
registration
cluster non empty strict right_unital for multLoopStr_0 ;
existence
ex b1 being non empty strict multLoopStr_0 st b1 is right_unital
proof
take multEX_0 ; ::_thesis: multEX_0 is right_unital
thus multEX_0 is right_unital ; ::_thesis: verum
end;
end;
registration
cluster non empty non trivial right_complementable almost_left_invertible strict associative commutative well-unital distributive Abelian add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is commutative & b1 is distributive & b1 is almost_left_invertible & b1 is well-unital & not b1 is trivial )
proof
take F_Real ; ::_thesis: ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial )
thus ( F_Real is strict & F_Real is Abelian & F_Real is add-associative & F_Real is right_zeroed & F_Real is right_complementable & F_Real is associative & F_Real is commutative & F_Real is distributive & F_Real is almost_left_invertible & F_Real is well-unital & not F_Real is trivial ) ; ::_thesis: verum
end;
end;
theorem Th12: :: POLYNOM1:12
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
proof
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L
for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
let a be Element of L; ::_thesis: for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
set p = <*> the carrier of L;
defpred S1[ FinSequence of the carrier of L] means Sum (a * $1) = a * (Sum $1);
A1: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_L
for_r_being_Element_of_L_st_S1[p]_holds_
S1[p_^_<*r*>]
let p be FinSequence of the carrier of L; ::_thesis: for r being Element of L st S1[p] holds
S1[p ^ <*r*>]
let r be Element of L; ::_thesis: ( S1[p] implies S1[p ^ <*r*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*r*>]
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 S1[p ^ <*r*>] ; ::_thesis: verum
end;
( Sum (<*> the carrier of L) = 0. L & Sum (a * (<*> the carrier of L)) = Sum (<*> the carrier of L) ) by Th6, RLVECT_1:43;
then A3: S1[ <*> the carrier of L] by VECTSP_1:6;
thus for p being FinSequence of the carrier of L holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum
end;
theorem Th13: :: POLYNOM1:13
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for a being Element of L
for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
proof
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L
for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
let a be Element of L; ::_thesis: for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
set p = <*> the carrier of L;
defpred S1[ FinSequence of the carrier of L] means Sum ($1 * a) = (Sum $1) * a;
A1: now__::_thesis:_for_p_being_FinSequence_of_the_carrier_of_L
for_r_being_Element_of_L_st_S1[p]_holds_
S1[p_^_<*r*>]
let p be FinSequence of the carrier of L; ::_thesis: for r being Element of L st S1[p] holds
S1[p ^ <*r*>]
let r be Element of L; ::_thesis: ( S1[p] implies S1[p ^ <*r*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*r*>]
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 S1[p ^ <*r*>] ; ::_thesis: verum
end;
( Sum (<*> the carrier of L) = 0. L & Sum ((<*> the carrier of L) * a) = Sum (<*> the carrier of L) ) by Th7, RLVECT_1:43;
then A3: S1[ <*> the carrier of L] by VECTSP_1:7;
thus for p being FinSequence of the carrier of L holds S1[p] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum
end;
begin
theorem Th14: :: POLYNOM1:14
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)
proof
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for F being FinSequence of the carrier of L * holds Sum (FlattenSeq F) = Sum (Sum F)
defpred S1[ FinSequence of the carrier of L * ] means Sum (FlattenSeq $1) = Sum (Sum $1);
A1: for f being FinSequence of the carrier of L *
for p being Element of the carrier of L * st S1[f] holds
S1[f ^ <*p*>]
proof
let f be FinSequence of the carrier of L * ; ::_thesis: for p being Element of the carrier of L * st S1[f] holds
S1[f ^ <*p*>]
let p be Element of the carrier of L * ; ::_thesis: ( S1[f] implies S1[f ^ <*p*>] )
assume A2: Sum (FlattenSeq f) = Sum (Sum f) ; ::_thesis: S1[f ^ <*p*>]
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 ; ::_thesis: verum
end;
Sum (FlattenSeq (<*> ( the carrier of L *))) = Sum (<*> the carrier of L) ;
then A3: S1[ <*> ( the carrier of L *)] by Th3;
thus for f being FinSequence of the carrier of L * holds S1[f] from FINSEQ_2:sch_2(A3, A1); ::_thesis: verum
end;
definition
let X be non empty set ;
let S be ZeroStr ;
let f be Function of X,S;
func Support f -> Subset of X means :Def3: :: POLYNOM1:def 3
for x being Element of X holds
( x in it iff f . x <> 0. S );
existence
ex b1 being Subset of X st
for x being Element of X holds
( x in b1 iff f . x <> 0. S )
proof
defpred S1[ set ] means f . $1 <> 0. S;
consider B being Subset of X such that
A1: for x being Element of X holds
( x in B iff S1[x] ) from SUBSET_1:sch_3();
take B ; ::_thesis: for x being Element of X holds
( x in B iff f . x <> 0. S )
thus for x being Element of X holds
( x in B iff f . x <> 0. S ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of X st ( for x being Element of X holds
( x in b1 iff f . x <> 0. S ) ) & ( for x being Element of X holds
( x in b2 iff f . x <> 0. S ) ) holds
b1 = b2
proof
let A, B be Subset of X; ::_thesis: ( ( for x being Element of X holds
( x in A iff f . x <> 0. S ) ) & ( for x being Element of X holds
( x in B iff f . x <> 0. S ) ) implies A = B )
assume that
A2: for x being Element of X holds
( x in A iff f . x <> 0. S ) and
A3: for x being Element of X holds
( x in B iff f . x <> 0. S ) ; ::_thesis: A = B
now__::_thesis:_for_x_being_Element_of_X_holds_
(_x_in_A_iff_x_in_B_)
let x be Element of X; ::_thesis: ( x in A iff x in B )
( x in A iff f . x <> 0. S ) by A2;
hence ( x in A iff x in B ) by A3; ::_thesis: verum
end;
hence A = B by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Support POLYNOM1:def_3_:_
for X being non empty set
for S being ZeroStr
for f being Function of X,S
for b4 being Subset of X holds
( b4 = Support f iff for x being Element of X holds
( x in b4 iff f . x <> 0. S ) );
definition
let X be non empty set ;
let S be ZeroStr ;
let p be Function of X,S;
attrp is finite-Support means :Def4: :: POLYNOM1:def 4
Support p is finite ;
end;
:: deftheorem Def4 defines finite-Support POLYNOM1:def_4_:_
for X being non empty set
for S being ZeroStr
for p being Function of X,S holds
( p is finite-Support iff Support p is finite );
definition
let n be set ;
let L be non empty 1-sorted ;
let p be Function of (Bags n),L;
let x be bag of n;
:: original: .
redefine funcp . x -> Element of L;
coherence
p . x is Element of L
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 p . x is Element of L ; ::_thesis: verum
end;
end;
begin
definition
let X be set ;
let S be 1-sorted ;
mode Series of X,S is Function of (Bags X),S;
end;
definition
let n be set ;
let L be non empty addLoopStr ;
let p, q be Series of n,L;
funcp + q -> Series of n,L equals :: POLYNOM1:def 5
p + q;
coherence
p + q is Series of n,L ;
end;
:: deftheorem defines + POLYNOM1:def_5_:_
for n being set
for L being non empty addLoopStr
for p, q being Series of n,L holds p + q = p + q;
theorem Th15: :: POLYNOM1:15
for n being set
for L being non empty addLoopStr
for 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 ; ::_thesis: for L being non empty addLoopStr
for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let L be non empty addLoopStr ; ::_thesis: for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let p, q be Series of n,L; ::_thesis: for x being bag of n holds (p + q) . x = (p . x) + (q . x)
let x be bag of n; ::_thesis: (p + q) . x = (p . x) + (q . x)
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 ;
::_thesis: verum
end;
theorem :: POLYNOM1:16
for n being set
for L being non empty addLoopStr
for 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 ; ::_thesis: for L being non empty addLoopStr
for 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
let L be non empty addLoopStr ; ::_thesis: for 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
let p, q, r be Series of n,L; ::_thesis: ( ( for x being bag of n holds r . x = (p . x) + (q . x) ) implies r = p + q )
assume A1: for x being bag of n holds r . x = (p . x) + (q . x) ; ::_thesis: r = p + q
let x be Element of Bags n; :: according to FUNCT_2:def_8 ::_thesis: r . x = (p + q) . x
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 ; ::_thesis: verum
end;
theorem Th17: :: POLYNOM1:17
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
proof
let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L
for x being bag of n holds (- p) . x = - (p . x)
let p be Series of n,L; ::_thesis: for x being bag of n holds (- p) . x = - (p . x)
let x be bag of n; ::_thesis: (- p) . x = - (p . x)
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 ;
::_thesis: verum
end;
theorem :: POLYNOM1:18
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for 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 ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p
let p, r be Series of n,L; ::_thesis: ( ( for x being bag of n holds r . x = - (p . x) ) implies r = - p )
assume A1: for x being bag of n holds r . x = - (p . x) ; ::_thesis: r = - p
let x be Element of Bags n; :: according to FUNCT_2:def_8 ::_thesis: r . x = (- p) . x
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 ; ::_thesis: verum
end;
theorem :: POLYNOM1:19
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p = - (- p)
proof
let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p = - (- p)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p = - (- p)
let p be Series of n,L; ::_thesis: p = - (- p)
set r = - p;
A1: dom p = Bags n by FUNCT_2:def_1;
A2: dom (- p) = Bags n by FUNCT_2:def_1;
A3: dom (- p) = dom p by VFUNCT_1:def_5;
A4: dom (- (- p)) = dom (- p) by VFUNCT_1:def_5;
A5: dom (- (- p)) = dom (- p) by VFUNCT_1:def_5;
now__::_thesis:_for_x_being_Element_of_Bags_n_st_x_in_dom_p_holds_
p_._x_=_(-_(-_p))_._x
let x be Element of Bags n; ::_thesis: ( x in dom p implies p . x = (- (- p)) . x )
assume x in dom p ; ::_thesis: p . x = (- (- p)) . x
A6: p . x = p /. x ;
thus p . x = - (- (p . x)) by RLVECT_1:17
.= - ((- p) /. x) by A1, A3, A6, VFUNCT_1:def_5
.= (- (- p)) /. x by A1, A3, A5, VFUNCT_1:def_5
.= (- (- p)) . x ; ::_thesis: verum
end;
hence p = - (- p) by A1, A2, A4, PARTFUN1:5; ::_thesis: verum
end;
theorem Th20: :: POLYNOM1:20
for n being set
for L being non empty right_zeroed addLoopStr
for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
proof
let n be set ; ::_thesis: for L being non empty right_zeroed addLoopStr
for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p, q being Series of n,L holds Support (p + q) c= (Support p) \/ (Support q)
let p, q be Series of n,L; ::_thesis: Support (p + q) c= (Support p) \/ (Support q)
set f = p + q;
set Sp = Support p;
set Sq = Support q;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support (p + q) or x in (Support p) \/ (Support q) )
assume A1: x in Support (p + q) ; ::_thesis: x in (Support p) \/ (Support q)
then reconsider x9 = x as Element of Bags n ;
(p + q) . x9 <> 0. L by A1, Def3;
then (p . x9) + (q . x9) <> 0. L by Th15;
then ( not p . x9 = 0. L or not q . x9 = 0. L ) by RLVECT_1:def_4;
then ( x9 in Support p or x9 in Support q ) by Def3;
hence x in (Support p) \/ (Support q) by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let n be set ;
let L be non empty Abelian right_zeroed addLoopStr ;
let p, q be Series of n,L;
:: original: +
redefine funcp + q -> Series of n,L;
commutativity
for p, q being Series of n,L holds p + q = q + p
proof
let p, q be Series of n,L; ::_thesis: p + q = q + p
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_+_q)_._b_=_(q_+_p)_._b
let b be Element of Bags n; ::_thesis: (p + q) . b = (q + p) . b
thus (p + q) . b = (q . b) + (p . b) by Th15
.= (q + p) . b by Th15 ; ::_thesis: verum
end;
hence p + q = q + p by FUNCT_2:63; ::_thesis: verum
end;
end;
theorem Th21: :: POLYNOM1:21
for n being set
for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
proof
let n be set ; ::_thesis: for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
let L be non empty add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)
let p, q, r be Series of n,L; ::_thesis: (p + q) + r = p + (q + r)
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((p_+_q)_+_r)_._b_=_(p_+_(q_+_r))_._b
let b be Element of Bags n; ::_thesis: ((p + q) + r) . b = (p + (q + r)) . b
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 ; ::_thesis: verum
end;
hence (p + q) + r = p + (q + r) by FUNCT_2:63; ::_thesis: verum
end;
definition
let n be set ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Series of n,L;
funcp - q -> Series of n,L equals :: POLYNOM1:def 6
p + (- q);
coherence
p + (- q) is Series of n,L ;
end;
:: deftheorem defines - POLYNOM1:def_6_:_
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Series of n,L holds p - q = p + (- q);
definition
let n be set ;
let S be non empty ZeroStr ;
func 0_ (n,S) -> Series of n,S equals :: POLYNOM1:def 7
(Bags n) --> (0. S);
coherence
(Bags n) --> (0. S) is Series of n,S ;
end;
:: deftheorem defines 0_ POLYNOM1:def_7_:_
for n being set
for S being non empty ZeroStr holds 0_ (n,S) = (Bags n) --> (0. S);
theorem Th22: :: POLYNOM1:22
for n being set
for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S
proof
let n be set ; ::_thesis: for S being non empty ZeroStr
for b being bag of n holds (0_ (n,S)) . b = 0. S
let S be non empty ZeroStr ; ::_thesis: for b being bag of n holds (0_ (n,S)) . b = 0. S
let b be bag of n; ::_thesis: (0_ (n,S)) . b = 0. S
b in Bags n by PRE_POLY:def_12;
hence (0_ (n,S)) . b = 0. S by FUNCOP_1:7; ::_thesis: verum
end;
theorem Th23: :: POLYNOM1:23
for n being set
for L being non empty right_zeroed addLoopStr
for p being Series of n,L holds p + (0_ (n,L)) = p
proof
let n be set ; ::_thesis: for L being non empty right_zeroed addLoopStr
for p being Series of n,L holds p + (0_ (n,L)) = p
let L be non empty right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p + (0_ (n,L)) = p
let p be Series of n,L; ::_thesis: p + (0_ (n,L)) = p
reconsider ls = p + (0_ (n,L)), p9 = p as Function of (Bags n), the carrier of L ;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_ls_._b_=_p9_._b
let b be Element of Bags n; ::_thesis: ls . b = p9 . b
thus ls . b = (p . b) + ((0_ (n,L)) . b) by Th15
.= (p9 . b) + (0. L) by Th22
.= p9 . b by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence p + (0_ (n,L)) = p by FUNCT_2:63; ::_thesis: verum
end;
definition
let n be set ;
let L be non empty right_unital multLoopStr_0 ;
func 1_ (n,L) -> Series of n,L equals :: POLYNOM1:def 8
(0_ (n,L)) +* ((EmptyBag n),(1. L));
coherence
(0_ (n,L)) +* ((EmptyBag n),(1. L)) is Series of n,L ;
end;
:: deftheorem defines 1_ POLYNOM1:def_8_:_
for n being set
for L being non empty right_unital multLoopStr_0 holds 1_ (n,L) = (0_ (n,L)) +* ((EmptyBag n),(1. L));
theorem Th24: :: POLYNOM1:24
for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p - p = 0_ (n,L)
proof
let n be set ; ::_thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L holds p - p = 0_ (n,L)
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for p being Series of n,L holds p - p = 0_ (n,L)
let p be Series of n,L; ::_thesis: p - p = 0_ (n,L)
reconsider pp = p - p, Z = 0_ (n,L) as Function of (Bags n), the carrier of L ;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pp_._b_=_Z_._b
let b be Element of Bags n; ::_thesis: pp . b = Z . b
thus pp . b = (p . b) + ((- p) . b) by Th15
.= (p . b) + (- (p . b)) by Th17
.= 0. L by RLVECT_1:def_10
.= Z . b by Th22 ; ::_thesis: verum
end;
hence p - p = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th25: :: POLYNOM1:25
for n being set
for L being non empty right_unital 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 ; ::_thesis: for L being non empty right_unital 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 ) )
let L be non empty right_unital multLoopStr_0 ; ::_thesis: ( (1_ (n,L)) . (EmptyBag n) = 1. L & ( for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L ) )
set Z = 0_ (n,L);
dom (0_ (n,L)) = Bags n by FUNCOP_1:13;
hence (1_ (n,L)) . (EmptyBag n) = 1. L by FUNCT_7:31; ::_thesis: for b being bag of n st b <> EmptyBag n holds
(1_ (n,L)) . b = 0. L
let b be bag of n; ::_thesis: ( b <> EmptyBag n implies (1_ (n,L)) . b = 0. L )
A1: b in Bags n by PRE_POLY:def_12;
assume b <> EmptyBag n ; ::_thesis: (1_ (n,L)) . b = 0. L
hence (1_ (n,L)) . b = (0_ (n,L)) . b by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
definition
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let p, q be Series of n,L;
funcp *' q -> Series of n,L means :Def9: :: POLYNOM1:def 9
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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) );
existence
ex b1 being Series of n,L st
for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
proof
defpred S1[ 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) );
A1: now__::_thesis:_for_bb_being_Element_of_Bags_n_ex_y_being_Element_of_L_st_S1[bb,y]
let bb be Element of Bags n; ::_thesis: ex y being Element of L st S1[bb,y]
reconsider b = bb as bag of n ;
defpred S2[ Nat, set ] means ex b1, b2 being bag of n st
( (decomp b) /. $1 = <*b1,b2*> & $2 = (p . b1) * (q . b2) );
A2: now__::_thesis:_for_k_being_Nat_st_k_in_Seg_(len_(decomp_b))_holds_
ex_x_being_Element_of_L_st_S2[k,x]
let k be Nat; ::_thesis: ( k in Seg (len (decomp b)) implies ex x being Element of L st S2[k,x] )
assume k in Seg (len (decomp b)) ; ::_thesis: ex x being Element of L st S2[k,x]
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 = x; ::_thesis: S2[k,x]
thus S2[k,x] by A3; ::_thesis: verum
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
S2[k,s /. k] from FINSEQ_4:sch_1(A2);
reconsider y = Sum s as Element of L ;
take y = y; ::_thesis: S1[bb,y]
thus S1[bb,y] ::_thesis: verum
proof
take b ; ::_thesis: ( b = bb & ex s being FinSequence of the carrier of L st
( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) )
thus b = bb ; ::_thesis: ex s being FinSequence of the carrier of L st
( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
take s ; ::_thesis: ( y = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
thus y = Sum s ; ::_thesis: ( len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
thus len s = len (decomp b) by A4; ::_thesis: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) )
let k be Element of NAT ; ::_thesis: ( k in dom s implies ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) )
assume k in dom s ; ::_thesis: ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) )
then k in Seg (len (decomp b)) by A4, FINSEQ_1:def_3;
hence ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by A5; ::_thesis: verum
end;
end;
consider P being Function of (Bags n), the carrier of L such that
A6: for b being Element of Bags n holds S1[b,P . b] from FUNCT_2:sch_3(A1);
reconsider P = P as Function of (Bags n),L ;
reconsider P = P as Series of n,L ;
take P ; ::_thesis: for b being bag of n ex s being FinSequence of the carrier of L st
( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
let b be bag of n; ::_thesis: ex s being FinSequence of the carrier of L st
( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) )
reconsider bb = b as Element of Bags n by PRE_POLY:def_12;
S1[bb,P . bb] by A6;
hence ex s being FinSequence of the carrier of L st
( P . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Series of n,L st ( for b being bag of n ex s being FinSequence of the carrier of L st
( b1 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( for b being bag of n ex s being FinSequence of the carrier of L st
( b2 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) holds
b1 = b2
proof
let it1, it2 be Series of n,L; ::_thesis: ( ( 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) & ( 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ) implies it1 = it2 )
assume 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 holds
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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) ; ::_thesis: it1 = it2
reconsider ita = it1, itb = it2 as Function of (Bags n), the carrier of L ;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_ita_._b_=_itb_._b
let b be Element of Bags n; ::_thesis: ita . b = itb . b
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 holds
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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & sb /. k = (p . b1) * (q . b2) ) by A8;
now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_sa_holds_
sa_._k_=_sb_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len sa implies sa . k = sb . k )
assume A15: ( 1 <= k & k <= len sa ) ; ::_thesis: sa . k = sb . k
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; ::_thesis: verum
end;
hence ita . b = itb . b by A9, A10, A12, A13, FINSEQ_1:14; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines *' POLYNOM1:def_9_:_
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p, q, b5 being Series of n,L holds
( b5 = p *' q iff for b being bag of n ex s being FinSequence of the carrier of L st
( b5 . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) ) ) );
theorem Th26: :: POLYNOM1:26
for n being Ordinal
for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
let L be non empty right_complementable associative distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
let p, q, r be Series of n,L; ::_thesis: p *' (q + r) = (p *' q) + (p *' r)
set cL = the carrier of L;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(q_+_r))_._b_=_((p_*'_q)_+_(p_*'_r))_._b
let b be Element of Bags n; ::_thesis: (p *' (q + r)) . b = ((p *' q) + (p *' r)) . b
consider s being FinSequence of the carrier of L 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((q + r) . b2) ) by Def9;
consider u being FinSequence of the carrier of L 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & u /. k = (p . b1) * (r . b2) ) by Def9;
consider t being FinSequence of the carrier of L 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & t /. k = (p . b1) * (q . b2) ) by Def9;
reconsider t = t, u = u as Element of (len s) -tuples_on the carrier of L 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__::_thesis:_for_i_being_Nat_st_i_in_dom_s_holds_
s_._i_=_(t_+_u)_._i
let i be Nat; ::_thesis: ( i in dom s implies s . i = (t + u) . i )
assume A14: i in dom s ; ::_thesis: s . i = (t + u) . i
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 ;
::_thesis: verum
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 ;
::_thesis: verum
end;
hence p *' (q + r) = (p *' q) + (p *' r) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th27: :: POLYNOM1:27
for n being Ordinal
for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
let L be non empty right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for p, q, r being Series of n,L holds (p *' q) *' r = p *' (q *' r)
let p, q, r be Series of n,L; ::_thesis: (p *' q) *' r = p *' (q *' r)
set cL = the carrier of L;
reconsider pqra = (p *' q) *' r, pqrb = p *' (q *' r) as Function of (Bags n), the carrier of L ;
set pq = p *' q;
set qr = q *' r;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pqra_._b_=_pqrb_._b
let b be Element of Bags n; ::_thesis: pqra . b = pqrb . b
set db = decomp b;
deffunc H1( Nat) -> set = (decomp (((decomp b) /. $1) /. 1)) ^^ ((len (decomp (((decomp b) /. $1) /. 1))) |-> <*(((decomp b) /. $1) /. 2)*>);
consider dbl being FinSequence such that
A1: len dbl = len (decomp b) and
A2: for k being Nat st k in dom dbl holds
dbl . k = H1(k) from FINSEQ_1:sch_2();
A3: rng dbl c= (3 -tuples_on (Bags n)) *
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng dbl or y in (3 -tuples_on (Bags n)) * )
assume y in rng dbl ; ::_thesis: y in (3 -tuples_on (Bags n)) *
then consider k being set such that
A4: k in dom dbl and
A5: y = dbl . k by FUNCT_1:def_3;
set dbk2 = ((decomp b) /. k) /. 2;
set ddbk1 = decomp (((decomp b) /. k) /. 1);
reconsider k = k as Nat by A4;
set dblk = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>);
A6: dom ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) = (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) by PRE_POLY:def_4
.= (dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1)))) by FUNCOP_1:13
.= (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3
.= dom (decomp (((decomp b) /. k) /. 1)) ;
A7: dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3;
rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) c= 3 -tuples_on (Bags n)
proof
reconsider Gi = <*(((decomp b) /. k) /. 2)*> as Element of 1 -tuples_on (Bags n) by FINSEQ_2:98;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) or y in 3 -tuples_on (Bags n) )
assume y in rng ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) ; ::_thesis: y in 3 -tuples_on (Bags n)
then consider i being set such that
A8: i in dom ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) and
A9: ((decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) . i = y by FUNCT_1:def_3;
(decomp (((decomp b) /. k) /. 1)) . i in rng (decomp (((decomp b) /. k) /. 1)) by A6, A8, FUNCT_1:def_3;
then reconsider Fi = (decomp (((decomp b) /. k) /. 1)) . i as Element of 2 -tuples_on (Bags n) ;
reconsider i9 = i as Element of NAT by A8;
((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i9 = <*(((decomp b) /. k) /. 2)*> by A6, A7, A8, FUNCOP_1:7;
then y = Fi ^ Gi by A8, A9, PRE_POLY:def_4;
hence y in 3 -tuples_on (Bags n) by FINSEQ_2:131; ::_thesis: verum
end;
then A10: (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) is FinSequence of 3 -tuples_on (Bags n) by FINSEQ_1:def_4;
dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) by A2, A4;
hence y in (3 -tuples_on (Bags n)) * by A5, A10, FINSEQ_1:def_11; ::_thesis: verum
end;
deffunc H2( Element of 3 -tuples_on (Bags n)) -> Element of the carrier of L = ((p . ($1 /. 1)) * (q . ($1 /. 2))) * (r . ($1 /. 3));
consider v being Function of (3 -tuples_on (Bags n)), the carrier of L such that
A11: for b being Element of 3 -tuples_on (Bags n) holds v . b = H2(b) from FUNCT_2:sch_4();
deffunc H3( Nat) -> set = ((len (decomp (((decomp b) /. $1) /. 2))) |-> <*(((decomp b) /. $1) /. 1)*>) ^^ (decomp (((decomp b) /. $1) /. 2));
consider dbr being FinSequence such that
A12: len dbr = len (decomp b) and
A13: for k being Nat st k in dom dbr holds
dbr . k = H3(k) from FINSEQ_1:sch_2();
rng dbr c= (3 -tuples_on (Bags n)) *
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng dbr or y in (3 -tuples_on (Bags n)) * )
assume y in rng dbr ; ::_thesis: y in (3 -tuples_on (Bags n)) *
then consider k being set such that
A14: k in dom dbr and
A15: y = dbr . k by FUNCT_1:def_3;
reconsider k = k as Nat by A14;
set ddbk1 = decomp (((decomp b) /. k) /. 2);
set dbk2 = ((decomp b) /. k) /. 1;
set dbrk = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2));
A16: dom (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) = (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>)) by PRE_POLY:def_4
.= (dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2)))) by FUNCOP_1:13
.= (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3
.= dom (decomp (((decomp b) /. k) /. 2)) ;
A17: dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3;
rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) c= 3 -tuples_on (Bags n)
proof
reconsider Gi = <*(((decomp b) /. k) /. 1)*> as Element of 1 -tuples_on (Bags n) by FINSEQ_2:98;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) or y in 3 -tuples_on (Bags n) )
assume y in rng (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) ; ::_thesis: y in 3 -tuples_on (Bags n)
then consider i being set such that
A18: i in dom (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) and
A19: (((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2))) . i = y by FUNCT_1:def_3;
(decomp (((decomp b) /. k) /. 2)) . i in rng (decomp (((decomp b) /. k) /. 2)) by A16, A18, FUNCT_1:def_3;
then reconsider Fi = (decomp (((decomp b) /. k) /. 2)) . i as Element of 2 -tuples_on (Bags n) ;
reconsider i9 = i as Element of NAT by A18;
((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i9 = <*(((decomp b) /. k) /. 1)*> by A16, A17, A18, FUNCOP_1:7;
then y = Gi ^ Fi by A18, A19, PRE_POLY:def_4;
hence y in 3 -tuples_on (Bags n) by FINSEQ_2:131; ::_thesis: verum
end;
then A20: ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) is FinSequence of 3 -tuples_on (Bags n) by FINSEQ_1:def_4;
dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) by A13, A14;
hence y in (3 -tuples_on (Bags n)) * by A15, A20, FINSEQ_1:def_11; ::_thesis: verum
end;
then reconsider dbl = dbl, dbr = dbr as FinSequence of (3 -tuples_on (Bags n)) * by A3, FINSEQ_1:def_4;
set fdbl = FlattenSeq dbl;
set fdbr = FlattenSeq dbr;
consider ls being FinSequence of the carrier of L 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & ls /. k = ((p *' q) . b1) * (r . b2) ) by Def9;
A24: dom dbr = dom (decomp b) by A12, FINSEQ_3:29;
reconsider vfdbl = v * (FlattenSeq dbl), vfdbr = v * (FlattenSeq dbr) as FinSequence of the carrier of L by FINSEQ_2:32;
consider vdbl being FinSequence of the carrier of L * 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__::_thesis:_(_len_(Sum_vdbl)_=_len_ls_&_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_ls_holds_
(Sum_vdbl)_._k_=_ls_._k_)_)
set f = Sum vdbl;
A28: dom vdbl = (dom ((dom dbl) --> v)) /\ (dom dbl) by A25, PBOOLE:def_19
.= (dom dbl) /\ (dom dbl) by FUNCOP_1:13
.= dom dbl ;
A29: dom (Sum vdbl) = dom vdbl by Th2;
hence len (Sum vdbl) = len ls by A22, A1, A28, FINSEQ_3:29; ::_thesis: for k being Nat st 1 <= k & k <= len ls holds
(Sum vdbl) . k = ls . k
let k be Nat; ::_thesis: ( 1 <= k & k <= len ls implies (Sum vdbl) . k = ls . k )
assume A30: ( 1 <= k & k <= len ls ) ; ::_thesis: (Sum vdbl) . k = ls . k
A31: k in dom (Sum vdbl) by A22, A1, A29, A28, A30, FINSEQ_3:25;
then A32: (Sum vdbl) /. k = (Sum vdbl) . k by PARTFUN1:def_6;
A33: dom ls = dom (Sum vdbl) by A22, A1, A29, A28, FINSEQ_3:29;
then A34: ls /. k = ls . k by A31, PARTFUN1:def_6;
consider b1, b2 being bag of n such that
A35: (decomp b) /. k = <*b1,b2*> and
A36: ls /. k = ((p *' q) . 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: ((decomp b) /. k) /. 1 = <*b1,b2*> . 1 by A35, PARTFUN1:def_6
.= b1 by FINSEQ_1:44 ;
set dblk = dbl . k;
set dbk2 = ((decomp b) /. k) /. 2;
set ddbk1 = decomp (((decomp b) /. k) /. 1);
A39: k in dom vdbl by A22, A1, A28, A30, FINSEQ_3:25;
then A40: dbl . k = (decomp (((decomp b) /. k) /. 1)) ^^ ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) by A2, A28;
then A41: dom (dbl . k) = (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom ((len (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>)) by PRE_POLY:def_4
.= (dom (decomp (((decomp b) /. k) /. 1))) /\ (Seg (len (decomp (((decomp b) /. k) /. 1)))) by FUNCOP_1:13
.= (dom (decomp (((decomp b) /. k) /. 1))) /\ (dom (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3
.= dom (decomp (((decomp b) /. k) /. 1)) ;
set vdblk = v * (dbl . k);
k in dom dbl by A22, A1, A30, FINSEQ_3:25;
then dbl . k in rng dbl by FUNCT_1:def_3;
then dbl . k is Element of (3 -tuples_on (Bags n)) * ;
then reconsider dblk = dbl . k as FinSequence of 3 -tuples_on (Bags n) ;
rng dblk c= 3 -tuples_on (Bags n) ;
then A42: dom (v * (dbl . k)) = dom dblk by A27, RELAT_1:27;
then A43: dom (v * (dbl . k)) = Seg (len (decomp (((decomp b) /. k) /. 1))) 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: (p *' q) . b1 = Sum pqs and
A45: len pqs = len (decomp b1) and
A46: for i being Element of NAT st i in dom pqs holds
ex b11, b12 being bag of n st
( (decomp b1) /. i = <*b11,b12*> & pqs /. i = (p . b11) * (q . b12) ) by Def9;
A47: dom pqs = dom (pqs * (r . b2)) by Def2;
2 in dom <*b1,b2*> by A37, FINSEQ_3:25;
then A48: ((decomp b) /. k) /. 2 = <*b1,b2*> . 2 by A35, PARTFUN1:def_6
.= b2 by FINSEQ_1:44 ;
reconsider vdblk = v * (dbl . k) as FinSequence by A43, FINSEQ_1:def_2;
A49: Sum (pqs * (r . b2)) = (Sum pqs) * (r . b2) by Th13;
A50: dom (decomp (((decomp b) /. k) /. 1)) = Seg (len (decomp (((decomp b) /. k) /. 1))) by FINSEQ_1:def_3;
now__::_thesis:_(_len_vdblk_=_len_(pqs_*_(r_._b2))_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(pqs_*_(r_._b2))_holds_
(v_*_(dbl_._k))_._i_=_(pqs_*_(r_._b2))_._i_)_)
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 ; ::_thesis: for i being Nat st 1 <= i & i <= len (pqs * (r . b2)) holds
(v * (dbl . k)) . i = (pqs * (r . b2)) . i
then A52: dom vdblk = dom (pqs * (r . b2)) by FINSEQ_3:29;
let i be Nat; ::_thesis: ( 1 <= i & i <= len (pqs * (r . b2)) implies (v * (dbl . k)) . i = (pqs * (r . b2)) . i )
reconsider i9 = i as Element of NAT by ORDINAL1:def_12;
assume A53: ( 1 <= i & i <= len (pqs * (r . b2)) ) ; ::_thesis: (v * (dbl . k)) . i = (pqs * (r . b2)) . i
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 (decomp (((decomp b) /. k) /. 1))) |-> <*(((decomp b) /. k) /. 2)*>) . i9 = <*(((decomp b) /. k) /. 2)*> & (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 ; ::_thesis: verum
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; ::_thesis: verum
end;
then A60: Sum vdbl = ls by FINSEQ_1:14;
consider vdbr being FinSequence of the carrier of L * 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 the carrier of L 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & rs /. k = (p . b1) * ((q *' r) . b2) ) by Def9;
now__::_thesis:_(_len_(Sum_vdbr)_=_len_rs_&_(_for_k_being_Nat_st_1_<=_k_&_k_<=_len_rs_holds_
(Sum_vdbr)_._k_=_rs_._k_)_)
set f = Sum vdbr;
A67: dom vdbr = (dom ((dom dbr) --> v)) /\ (dom dbr) by A61, PBOOLE:def_19
.= (dom dbr) /\ (dom dbr) by FUNCOP_1:13
.= dom dbr ;
A68: dom (Sum vdbr) = dom vdbr by Th2;
hence len (Sum vdbr) = len rs by A65, A12, A67, FINSEQ_3:29; ::_thesis: for k being Nat st 1 <= k & k <= len rs holds
(Sum vdbr) . k = rs . k
let k be Nat; ::_thesis: ( 1 <= k & k <= len rs implies (Sum vdbr) . k = rs . k )
assume A69: ( 1 <= k & k <= len rs ) ; ::_thesis: (Sum vdbr) . k = rs . k
A70: k in dom (Sum vdbr) by A65, A12, A68, A67, A69, FINSEQ_3:25;
then A71: (Sum vdbr) /. k = (Sum vdbr) . k by PARTFUN1:def_6;
set dbrk = dbr . k;
set dbk2 = ((decomp b) /. k) /. 1;
set ddbk1 = decomp (((decomp b) /. k) /. 2);
A72: k in dom vdbr by A65, A12, A67, A69, FINSEQ_3:25;
then A73: dbr . k = ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) ^^ (decomp (((decomp b) /. k) /. 2)) by A13, A67;
then A74: dom (dbr . k) = (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom ((len (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>)) by PRE_POLY:def_4
.= (dom (decomp (((decomp b) /. k) /. 2))) /\ (Seg (len (decomp (((decomp b) /. k) /. 2)))) by FUNCOP_1:13
.= (dom (decomp (((decomp b) /. k) /. 2))) /\ (dom (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3
.= dom (decomp (((decomp b) /. k) /. 2)) ;
k in dom dbr by A65, A12, A69, FINSEQ_3:25;
then dbr . k in rng dbr by FUNCT_1:def_3;
then A75: dbr . k is Element of (3 -tuples_on (Bags n)) * ;
set vdbrk = v * (dbr . k);
A76: dom (decomp (((decomp b) /. k) /. 2)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by FINSEQ_1:def_3;
reconsider dbrk = dbr . k as FinSequence of 3 -tuples_on (Bags n) by A75;
rng dbrk c= 3 -tuples_on (Bags n) ;
then A77: dom (v * (dbr . k)) = dom dbrk by A27, RELAT_1:27;
then A78: dom (v * (dbr . k)) = Seg (len (decomp (((decomp b) /. k) /. 2))) by A74, FINSEQ_1:def_3;
A79: dom rs = dom (Sum vdbr) 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: (decomp b) /. k = <*b1,b2*> and
A82: rs /. k = (p . b1) * ((q *' r) . 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: (q *' r) . b2 = Sum qrs and
A84: len qrs = len (decomp b2) and
A85: for i being Element of NAT st i in dom qrs holds
ex b11, b12 being bag of n st
( (decomp b2) /. i = <*b11,b12*> & qrs /. i = (q . b11) * (r . b12) ) by Def9;
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: ((decomp b) /. k) /. 1 = <*b1,b2*> . 1 by A81, PARTFUN1:def_6
.= b1 by FINSEQ_1:44 ;
reconsider vdbrk = v * (dbr . k) 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: ((decomp b) /. k) /. 2 = <*b1,b2*> . 2 by A81, PARTFUN1:def_6
.= b2 by FINSEQ_1:44 ;
then A92: dom vdbrk = dom ((p . b1) * qrs) by A84, A74, A77, A86, FINSEQ_3:29;
A93: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_((p_._b1)_*_qrs)_holds_
(v_*_(dbr_._k))_._i_=_((p_._b1)_*_qrs)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((p . b1) * qrs) implies (v * (dbr . k)) . i = ((p . b1) * qrs) . i )
reconsider i9 = i as Element of NAT by ORDINAL1:def_12;
assume A94: ( 1 <= i & i <= len ((p . b1) * qrs) ) ; ::_thesis: (v * (dbr . k)) . i = ((p . b1) * qrs) . i
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 (decomp (((decomp b) /. k) /. 2))) |-> <*(((decomp b) /. k) /. 1)*>) . i9 = <*(((decomp b) /. k) /. 1)*> & (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 ; ::_thesis: verum
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; ::_thesis: verum
end;
then A101: Sum vdbr = rs by FINSEQ_1:14;
dom dbl = dom (decomp b) by A1, FINSEQ_3:29;
then consider P being Permutation of (dom (FlattenSeq dbl)) such that
A102: FlattenSeq dbr = (FlattenSeq dbl) * P by A2, A13, A24, PRE_POLY:74;
rng (FlattenSeq dbl) c= 3 -tuples_on (Bags n) ;
then dom vfdbl = dom (FlattenSeq dbl) by A27, RELAT_1:27;
then reconsider P = 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; ::_thesis: verum
end;
hence (p *' q) *' r = p *' (q *' r) by FUNCT_2:63; ::_thesis: verum
end;
definition
let n be Ordinal;
let L be non empty right_complementable commutative Abelian add-associative right_zeroed doubleLoopStr ;
let p, q be Series of n,L;
:: original: *'
redefine funcp *' q -> Series of n,L;
commutativity
for p, q being Series of n,L holds p *' q = q *' p
proof
let p, q be Series of n,L; ::_thesis: p *' q = q *' p
reconsider pq = p *' q, qp = q *' p as Function of (Bags n), the carrier of L ;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_pq_._b_=_qp_._b
let b be Element of Bags n; ::_thesis: pq . b = qp . b
defpred S1[ set , set ] 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by Def9;
A4: dom s = dom (decomp b) by A2, FINSEQ_3:29;
then reconsider ds = dom s as non empty set ;
A5: now__::_thesis:_for_e_being_set_st_e_in_ds_holds_
ex_d_being_set_st_
(_d_in_ds_&_S1[e,d]_)
let e be set ; ::_thesis: ( e in ds implies ex d being set st
( d in ds & S1[e,d] ) )
assume A6: e in ds ; ::_thesis: ex d being set st
( d in ds & S1[e,d] )
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 = d as set ;
take d = d; ::_thesis: ( d in ds & S1[e,d] )
thus d in ds by A2, A9, FINSEQ_3:29; ::_thesis: S1[e,d]
thus S1[e,d] ::_thesis: verum
proof
take b1 ; ::_thesis: ex b2 being bag of n st
( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> )
take b2 ; ::_thesis: ( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> )
thus ( (decomp b) . e = <*b1,b2*> & (decomp b) . d = <*b2,b1*> ) by A4, A6, A7, A9, A10, PARTFUN1:def_6; ::_thesis: verum
end;
end;
consider f being Function of ds,ds such that
A11: for e being set st e in ds holds
S1[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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ds or x in rng f )
assume A13: x in ds ; ::_thesis: x in rng f
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 x in rng f by A4, A13, A17, A14, A19, FUNCT_1:def_4; ::_thesis: verum
end;
then A20: rng f = ds by XBOOLE_0:def_10;
f is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A21: x1 in dom f and
A22: x2 in dom f and
A23: f . x1 = f . x2 ; ::_thesis: x1 = 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 x1 = x2 by A4, A21, A22, A26, A24, FUNCT_1:def_4; ::_thesis: verum
end;
then reconsider f = 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & t /. k = (q . b1) * (p . b2) ) by Def9;
A31: dom t = dom (decomp b) by A29, FINSEQ_3:29;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_t_holds_
t_._i_=_s_._(f_._i)
let i be Element of NAT ; ::_thesis: ( i in dom t implies t . i = s . (f . i) )
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 ; ::_thesis: t . i = s . (f . i)
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; ::_thesis: verum
end;
hence pq . b = qp . b by A1, A2, A28, A29, RLVECT_2:6; ::_thesis: verum
end;
hence p *' q = q *' p by FUNCT_2:63; ::_thesis: verum
end;
end;
theorem :: POLYNOM1:28
for n being Ordinal
for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)
proof
let n be Ordinal; ::_thesis: for L being non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds p *' (0_ (n,L)) = 0_ (n,L)
let p be Series of n,L; ::_thesis: p *' (0_ (n,L)) = 0_ (n,L)
set Z = 0_ (n,L);
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(0__(n,L)))_._b_=_(0__(n,L))_._b
let b be Element of Bags n; ::_thesis: (p *' (0_ (n,L))) . b = (0_ (n,L)) . b
consider s being FinSequence of the carrier of L such that
A1: (p *' (0_ (n,L))) . b = Sum s and
len s = len (decomp b) and
A2: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((0_ (n,L)) . b2) ) by Def9;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_s_holds_
s_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom s implies s /. k = 0. L )
assume k in dom s ; ::_thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
(decomp b) /. k = <*b1,b2*> and
A3: s /. k = (p . b1) * ((0_ (n,L)) . b2) by A2;
thus s /. k = (p . b1) * (0. L) by A3, Th22
.= 0. L by VECTSP_1:6 ; ::_thesis: verum
end;
then Sum s = 0. L by MATRLIN:11;
hence (p *' (0_ (n,L))) . b = (0_ (n,L)) . b by A1, Th22; ::_thesis: verum
end;
hence p *' (0_ (n,L)) = 0_ (n,L) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th29: :: POLYNOM1:29
for n being Ordinal
for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (1_ (n,L)) = p
proof
let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds p *' (1_ (n,L)) = p
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds p *' (1_ (n,L)) = p
let p be Series of n,L; ::_thesis: p *' (1_ (n,L)) = p
set O = 1_ (n,L);
set cL = the carrier of L;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_(p_*'_(1__(n,L)))_._b_=_p_._b
let b be Element of Bags n; ::_thesis: (p *' (1_ (n,L))) . b = p . b
consider s being FinSequence of the carrier of L such that
A1: (p *' (1_ (n,L))) . b = Sum s and
A2: len s = len (decomp b) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * ((1_ (n,L)) . b2) ) by Def9;
consider t being FinSequence of the carrier of L, s1 being Element of the carrier of L such that
A4: s = t ^ <*s1*> by A2, FINSEQ_2:19;
A5: now__::_thesis:_Sum_t_=_0._L
percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;
suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L
hence Sum t = 0. L by RLVECT_1:43; ::_thesis: verum
end;
supposeA6: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L
now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_
t_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L )
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 ; ::_thesis: t /. b1 = 0. L
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;
percases ( 1 < k or k = 1 ) by A11, XXREAL_0:1;
supposeA15: 1 < k ; ::_thesis: t /. b1 = 0. L
consider b1, b2 being bag of n such that
A16: (decomp b) /. k = <*b1,b2*> and
A17: s /. k = (p . b1) * ((1_ (n,L)) . 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 by VECTSP_1:6 ;
::_thesis: verum
end;
supposeA18: k = 1 ; ::_thesis: t /. b1 = 0. L
A19: now__::_thesis:_not_b_=_EmptyBag_n
assume b = EmptyBag n ; ::_thesis: contradiction
then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then (len t) + 1 = 0 + 1 by A2, A7, FINSEQ_1:39;
hence contradiction by A6; ::_thesis: verum
end;
consider b1, b2 being bag of n such that
A20: (decomp b) /. k = <*b1,b2*> and
A21: s /. k = (p . b1) * ((1_ (n,L)) . 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 by VECTSP_1:6 ;
hence t /. k = 0. L by A9; ::_thesis: verum
end;
end;
end;
hence Sum t = 0. L by MATRLIN:11; ::_thesis: verum
end;
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;
not s is 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) * ((1_ (n,L)) . 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 by VECTSP_1:def_4 ;
hence (p *' (1_ (n,L))) . b = p . b by A1, A23, A5, RLVECT_1:4; ::_thesis: verum
end;
hence p *' (1_ (n,L)) = p by FUNCT_2:63; ::_thesis: verum
end;
theorem Th30: :: POLYNOM1:30
for n being Ordinal
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (1_ (n,L)) *' p = p
proof
let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L holds (1_ (n,L)) *' p = p
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being Series of n,L holds (1_ (n,L)) *' p = p
let p be Series of n,L; ::_thesis: (1_ (n,L)) *' p = p
set O = 1_ (n,L);
set cL = the carrier of L;
now__::_thesis:_for_b_being_Element_of_Bags_n_holds_((1__(n,L))_*'_p)_._b_=_p_._b
let b be Element of Bags n; ::_thesis: ((1_ (n,L)) *' p) . b = p . b
consider s being FinSequence of the carrier of L such that
A1: ((1_ (n,L)) *' p) . b = Sum s and
A2: len s = len (decomp b) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((1_ (n,L)) . b1) * (p . b2) ) by Def9;
not s is empty by A2;
then consider s1 being Element of the carrier of L, t being FinSequence of the carrier of L 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__::_thesis:_Sum_t_=_0._L
percases ( t = <*> the carrier of L or t <> <*> the carrier of L ) ;
suppose t = <*> the carrier of L ; ::_thesis: Sum t = 0. L
hence Sum t = 0. L by RLVECT_1:43; ::_thesis: verum
end;
supposeA8: t <> <*> the carrier of L ; ::_thesis: Sum t = 0. L
now__::_thesis:_for_k_being_Nat_st_k_in_dom_t_holds_
t_/._k_=_0._L
let k be Nat; ::_thesis: ( k in dom t implies t /. b1 = 0. L )
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 ; ::_thesis: t /. b1 = 0. L
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;
percases ( k + 1 < len s or k + 1 = len s ) by A13, XXREAL_0:1;
supposeA17: k + 1 < len s ; ::_thesis: t /. b1 = 0. L
consider b1, b2 being bag of n such that
A18: (decomp b) /. (k + 1) = <*b1,b2*> and
A19: s /. (k + 1) = ((1_ (n,L)) . 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 by VECTSP_1:7 ;
::_thesis: verum
end;
supposeA20: k + 1 = len s ; ::_thesis: t /. b1 = 0. L
A21: now__::_thesis:_not_b_=_EmptyBag_n
assume b = EmptyBag n ; ::_thesis: contradiction
then decomp b = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then (len t) + 1 = 0 + 1 by A2, A9, FINSEQ_1:39;
hence contradiction by A8; ::_thesis: verum
end;
consider b1, b2 being bag of n such that
A22: (decomp b) /. (k + 1) = <*b1,b2*> and
A23: s /. (k + 1) = ((1_ (n,L)) . 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 by VECTSP_1:7 ;
hence t /. k = 0. L by A11; ::_thesis: verum
end;
end;
end;
hence Sum t = 0. L by MATRLIN:11; ::_thesis: verum
end;
end;
end;
A24: not s is empty by A2;
then consider b1, b2 being bag of n such that
A25: (decomp b) /. 1 = <*b1,b2*> and
A26: s /. 1 = ((1_ (n,L)) . 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 by VECTSP_1:def_6 ;
hence ((1_ (n,L)) *' p) . b = p . b by A1, A6, A7, RLVECT_1:4; ::_thesis: verum
end;
hence (1_ (n,L)) *' p = p by FUNCT_2:63; ::_thesis: verum
end;
begin
registration
let n be set ;
let S be non empty ZeroStr ;
cluster Relation-like Bags n -defined the carrier of S -valued Function-like non empty total quasi_total finite-Support for Element of bool [:(Bags n), the carrier of S:];
existence
ex b1 being Series of n,S st b1 is finite-Support
proof
reconsider P = (Bags n) --> (0. S) as Function of (Bags n), the carrier of S ;
reconsider P = P as Function of (Bags n),S ;
reconsider P = P as Series of n,S ;
take P ; ::_thesis: P is finite-Support
for x being Element of Bags n holds
( x in {} iff P . x <> 0. S ) by FUNCOP_1:7;
then Support P = {} (Bags n) by Def3;
hence Support P is finite ; :: according to POLYNOM1:def_4 ::_thesis: verum
end;
end;
definition
let n be Ordinal;
let S be non empty ZeroStr ;
mode Polynomial of n,S is finite-Support Series of n,S;
end;
registration
let n be Ordinal;
let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
clusterp + q -> finite-Support ;
coherence
p + q is finite-Support
proof
set Sp = Support p;
set Sq = Support q;
( Support p is finite & Support q is finite ) by Def4;
then (Support p) \/ (Support q) is finite ;
then Support (p + q) is finite by Th20, FINSET_1:1;
hence p + q is finite-Support by Def4; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of n,L;
cluster - p -> finite-Support ;
coherence
- p is finite-Support
proof
set f = - p;
A1: Support (- p) c= Support p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Support (- p) or x in Support p )
assume A2: x in Support (- p) ; ::_thesis: x in Support p
then reconsider x9 = x as Element of Bags n ;
(- p) . x9 <> 0. L by A2, Def3;
then - (p . x9) <> 0. L by Th17;
then p . x9 <> 0. L by RLVECT_1:12;
hence x in Support p by Def3; ::_thesis: verum
end;
Support p is finite by Def4;
hence - p is finite-Support by A1, Def4; ::_thesis: verum
end;
end;
registration
let n be Element of NAT ;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
clusterp - q -> finite-Support ;
coherence
p - q is finite-Support ;
end;
registration
let n be Ordinal;
let S be non empty ZeroStr ;
cluster 0_ (n,S) -> finite-Support ;
coherence
0_ (n,S) is finite-Support
proof
set Z = 0_ (n,S);
now__::_thesis:_for_x_being_set_holds_not_x_in_Support_(0__(n,S))
given x being set such that A1: x in Support (0_ (n,S)) ; ::_thesis: contradiction
reconsider x = x as Element of Bags n by A1;
(0_ (n,S)) . x = 0. S by FUNCOP_1:7;
hence contradiction by A1, Def3; ::_thesis: verum
end;
then Support (0_ (n,S)) = {} by XBOOLE_0:def_1;
hence 0_ (n,S) is finite-Support by Def4; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non trivial right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ;
cluster 1_ (n,L) -> finite-Support ;
coherence
1_ (n,L) is finite-Support
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 = O9 as Series of n,L ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Support_O9_implies_not_x_<>_EmptyBag_n_)_&_(_x_=_EmptyBag_n_implies_x_in_Support_O9_)_)
let x be set ; ::_thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )
hereby ::_thesis: ( x = EmptyBag n implies x in Support O9 )
assume A1: x in Support O9 ; ::_thesis: not x <> EmptyBag n
then reconsider x9 = x as Element of Bags n ;
assume x <> EmptyBag n ; ::_thesis: contradiction
then O9 . x = (0_ (n,L)) . x9 by FUNCT_7:32
.= 0. L by FUNCOP_1:7 ;
hence contradiction by A1, Def3; ::_thesis: verum
end;
assume A2: x = EmptyBag n ; ::_thesis: x in Support O9
dom (0_ (n,L)) = Bags n by FUNCOP_1:13;
then O9 . x <> 0. L by A2, FUNCT_7:31;
hence x in Support O9 by A2, Def3; ::_thesis: verum
end;
then Support O9 = {(EmptyBag n)} by TARSKI:def_1;
hence 1_ (n,L) is finite-Support by Def4; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
let p, q be Polynomial of n,L;
clusterp *' q -> finite-Support ;
coherence
p *' q is finite-Support
proof
deffunc H1( Element of Bags n, Element of Bags n) -> set = n + L;
set D = { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } ;
A1: Support q is finite by Def4;
A2: Support (p *' q) c= { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) }
proof
let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in Support (p *' q) or x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } )
assume A3: x9 in Support (p *' q) ; ::_thesis: x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support 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 holds
ex b1, b2 being bag of n st
( (decomp b) /. k = <*b1,b2*> & s /. k = (p . b1) * (q . b2) ) by Def9;
(p *' q) . b <> 0. L by A3, Def3;
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, VECTSP_1:6;
then A13: b2 in Support q by A12, Def3;
p . b1 <> 0. L by A8, A10, VECTSP_1:7;
then A14: b1 in Support p by A11, Def3;
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 x9 in { H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } by A14, A13, A16; ::_thesis: verum
end;
A17: Support p is finite by Def4;
{ H1(b1,b2) where b1, b2 is Element of Bags n : ( b1 in Support p & b2 in Support q ) } is finite from FRAENKEL:sch_22(A17, A1);
hence p *' q is finite-Support by A2, Def4; ::_thesis: verum
end;
end;
begin
definition
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Ring (n,L) -> non empty strict doubleLoopStr means :Def10: :: POLYNOM1:def 10
( ( 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
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for 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
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) )
proof
reconsider Z = (Bags n) --> (0. L) as Function of (Bags n), the carrier of L ;
defpred S1[ set , set , set ] means ex p, q, r being Polynomial of n,L st
( p = $1 & q = $2 & r = $3 & p *' q = r );
defpred S2[ 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 S3[ 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 S3[x] ) from SUBSET_1:sch_3();
the finite-Support Series of n,L in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider P = P as non empty Subset of (Funcs ((Bags n), the carrier of L)) by A1;
A2: now__::_thesis:_for_x,_y_being_Element_of_P_ex_u_being_Element_of_P_st_S2[x,y,u]
let x, y be Element of P; ::_thesis: ex u being Element of P st S2[x,y,u]
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 = p9, q9 = q9 as Polynomial of n,L by A4, A6;
set r = p9 + q9;
p9 + q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider u = p9 + q9 as Element of P by A1;
take u = u; ::_thesis: S2[x,y,u]
thus S2[x,y,u] by A3, A5; ::_thesis: verum
end;
consider fadd being Function of [:P,P:],P such that
A7: for x, y being Element of P holds S2[x,y,fadd . (x,y)] from BINOP_1:sch_3(A2);
A8: now__::_thesis:_for_x,_y_being_Element_of_P_ex_u_being_Element_of_P_st_S1[x,y,u]
let x, y be Element of P; ::_thesis: ex u being Element of P st S1[x,y,u]
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 = p9, q9 = q9 as Polynomial of n,L by A10, A12;
set r = p9 *' q9;
p9 *' q9 in Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
then reconsider u = p9 *' q9 as Element of P by A1;
take u = u; ::_thesis: S1[x,y,u]
thus S1[x,y,u] by A9, A11; ::_thesis: verum
end;
consider fmult being Function of [:P,P:],P such that
A13: for x, y being Element of P holds S1[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 = Z9 as Series of n,L ;
now__::_thesis:_for_x_being_set_holds_not_x_in_Support_Z9
given x being set such that A14: x in Support Z9 ; ::_thesis: contradiction
reconsider x = x as Element of Bags n by A14;
Z9 . x = 0. L by FUNCOP_1:7;
hence contradiction by A14, Def3; ::_thesis: verum
end;
then Support Z9 = {} by XBOOLE_0:def_1;
then Z9 is finite-Support by Def4;
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 = O9 as Series of n,L ;
reconsider O = O as Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Support_O9_implies_not_x_<>_EmptyBag_n_)_&_(_x_=_EmptyBag_n_implies_x_in_Support_O9_)_)
let x be set ; ::_thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )
hereby ::_thesis: ( x = EmptyBag n implies x in Support O9 )
assume A15: x in Support O9 ; ::_thesis: not x <> EmptyBag n
then reconsider x9 = x as Element of Bags n ;
assume x <> EmptyBag n ; ::_thesis: contradiction
then O9 . x = Z . x9 by FUNCT_7:32
.= 0. L by FUNCOP_1:7 ;
hence contradiction by A15, Def3; ::_thesis: verum
end;
assume A16: x = EmptyBag n ; ::_thesis: x in Support O9
dom Z = Bags n by FUNCOP_1:13;
then O9 . x <> 0. L by A16, FUNCT_7:31;
hence x in Support O9 by A16, Def3; ::_thesis: verum
end;
then Support O9 = {(EmptyBag n)} by TARSKI:def_1;
then O9 is finite-Support by Def4;
then reconsider O = O as Element of P by A1;
reconsider R = doubleLoopStr(# P,fadd,fmult,O,Ze #) as non empty strict doubleLoopStr ;
take R ; ::_thesis: ( ( for x being set holds
( x in the carrier of R iff x is Polynomial of n,L ) ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )
thus for x being set holds
( x in the carrier of R iff x is Polynomial of n,L ) ::_thesis: ( ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )
proof
let x be set ; ::_thesis: ( x in the carrier of R iff x is Polynomial of n,L )
hereby ::_thesis: ( x is Polynomial of n,L implies x in the carrier of R )
assume A17: x in the carrier of R ; ::_thesis: x is Polynomial of n,L
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 ; ::_thesis: verum
end;
assume A18: x is Polynomial of n,L ; ::_thesis: x in the carrier of R
then x is Element of Funcs ((Bags n), the carrier of L) by FUNCT_2:8;
hence x in the carrier of R by A1, A18; ::_thesis: verum
end;
hereby ::_thesis: ( ( for x, y being Element of R
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )
let x, y be Element of R; ::_thesis: for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q
let p, q be Polynomial of n,L; ::_thesis: ( x = p & y = q implies x + y = p + q )
assume A19: ( x = p & y = q ) ; ::_thesis: x + y = p + 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; ::_thesis: verum
end;
hereby ::_thesis: ( 0. R = 0_ (n,L) & 1. R = 1_ (n,L) )
let x, y be Element of R; ::_thesis: for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q
let p, q be Polynomial of n,L; ::_thesis: ( x = p & y = q implies x * y = p *' q )
assume A20: ( x = p & y = q ) ; ::_thesis: x * y = p *' 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; ::_thesis: verum
end;
thus 0. R = 0_ (n,L) ; ::_thesis: 1. R = 1_ (n,L)
thus 1. R = 1_ (n,L) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b1 = 0_ (n,L) & 1. b1 = 1_ (n,L) & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b2 = 0_ (n,L) & 1. b2 = 1_ (n,L) holds
b1 = b2
proof
let it1, it2 be non empty strict doubleLoopStr ; ::_thesis: ( ( for x being set holds
( x in the carrier of it1 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it1
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. it1 = 0_ (n,L) & 1. it1 = 1_ (n,L) & ( for x being set holds
( x in the carrier of it2 iff x is Polynomial of n,L ) ) & ( for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it2
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. it2 = 0_ (n,L) & 1. it2 = 1_ (n,L) implies it1 = it2 )
assume 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
for 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
for 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
for 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
for 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) ) ; ::_thesis: it1 = it2
A29: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_the_carrier_of_it1_implies_x_in_the_carrier_of_it2_)_&_(_x_in_the_carrier_of_it2_implies_x_in_the_carrier_of_it1_)_)
let x be set ; ::_thesis: ( ( x in the carrier of it1 implies x in the carrier of it2 ) & ( x in the carrier of it2 implies x in the carrier of it1 ) )
hereby ::_thesis: ( x in the carrier of it2 implies x in the carrier of it1 )
assume x in the carrier of it1 ; ::_thesis: x in the carrier of it2
then x is Polynomial of n,L by A21;
hence x in the carrier of it2 by A25; ::_thesis: verum
end;
assume x in the carrier of it2 ; ::_thesis: x in the carrier of it1
then x is Polynomial of n,L by A25;
hence x in the carrier of it1 by A21; ::_thesis: verum
end;
then A30: the carrier of it1 = the carrier of it2 by TARSKI:1;
A31: now__::_thesis:_for_a,_b_being_Element_of_it1_holds_the_multF_of_it1_._(a,b)_=_the_multF_of_it2_._(a,b)
let a, b be Element of it1; ::_thesis: the multF of it1 . (a,b) = the multF of it2 . (a,b)
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) ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_Element_of_it1_holds_the_addF_of_it1_._(a,b)_=_the_addF_of_it2_._(a,b)
let a, b be Element of it1; ::_thesis: the addF of it1 . (a,b) = the addF of it2 . (a,b)
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) ; ::_thesis: verum
end;
then the addF of it1 = the addF of it2 by A30, BINOP_1:2;
hence it1 = it2 by A24, A28, A30, A31, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Polynom-Ring POLYNOM1:def_10_:_
for n being Ordinal
for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for b3 being non empty strict doubleLoopStr holds
( b3 = Polynom-Ring (n,L) iff ( ( for x being set holds
( x in the carrier of b3 iff x is Polynomial of n,L ) ) & ( for x, y being Element of b3
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b3
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b3 = 0_ (n,L) & 1. b3 = 1_ (n,L) ) );
registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict Abelian ;
coherence
Polynom-Ring (n,L) is Abelian
proof
set Pm = Polynom-Ring (n,L);
let v, w be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider p = v, q = w as Polynomial of n,L by Def10;
thus v + w = q + p by Def10
.= w + v by Def10 ; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict add-associative ;
coherence
Polynom-Ring (n,L) is add-associative
proof
set Pm = Polynom-Ring (n,L);
let u, v, w be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider o = u, p = v, q = w as Polynomial of n,L by Def10;
A1: v + w = p + q by Def10;
u + v = o + p by Def10;
hence (u + v) + w = (o + p) + q by Def10
.= o + (p + q) by Th21
.= u + (v + w) by A1, Def10 ;
::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict right_zeroed ;
coherence
Polynom-Ring (n,L) is right_zeroed
proof
let v be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def_4 ::_thesis: v + (0. (Polynom-Ring (n,L))) = v
reconsider p = v as Polynomial of n,L by Def10;
0. (Polynom-Ring (n,L)) = 0_ (n,L) by Def10;
hence v + (0. (Polynom-Ring (n,L))) = p + (0_ (n,L)) by Def10
.= v by Th23 ;
::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty right_complementable strict ;
coherence
Polynom-Ring (n,L) is right_complementable
proof
let v be Element of (Polynom-Ring (n,L)); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider p = v as Polynomial of n,L by Def10;
reconsider w = - p as Element of (Polynom-Ring (n,L)) by Def10;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. (Polynom-Ring (n,L))
thus v + w = p - p by Def10
.= 0_ (n,L) by Th24
.= 0. (Polynom-Ring (n,L)) by Def10 ; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non empty non trivial right_complementable commutative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict commutative ;
coherence
Polynom-Ring (n,L) is commutative
proof
set Pm = Polynom-Ring (n,L);
let v, w be Element of (Polynom-Ring (n,L)); :: according to GROUP_1:def_12 ::_thesis: v * w = w * v
reconsider p = v, q = w as Polynomial of n,L by Def10;
thus v * w = q *' p by Def10
.= w * v by Def10 ; ::_thesis: verum
end;
end;
registration
let n be Ordinal;
let L be non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict associative ;
coherence
Polynom-Ring (n,L) is associative
proof
set Pm = Polynom-Ring (n,L);
let x, y, z be Element of (Polynom-Ring (n,L)); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider p = x, q = y, r = z as Polynomial of n,L by Def10;
A1: y * z = q *' r by Def10;
x * y = p *' q by Def10;
hence (x * y) * z = (p *' q) *' r by Def10
.= p *' (q *' r) by Th27
.= x * (y * z) by A1, Def10 ;
::_thesis: verum
end;
end;
Lm1: now__::_thesis:_for_n_being_Ordinal
for_L_being_non_empty_non_trivial_right_complementable_associative_well-unital_distributive_Abelian_add-associative_right_zeroed_doubleLoopStr_
for_x,_e_being_Element_of_(Polynom-Ring_(n,L))_st_e_=_1._(Polynom-Ring_(n,L))_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let n be Ordinal; ::_thesis: for L being non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )
let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Polynom-Ring (n,L)) st e = 1. (Polynom-Ring (n,L)) holds
( x * e = x & e * x = x )
set Pm = Polynom-Ring (n,L);
let x, e be Element of (Polynom-Ring (n,L)); ::_thesis: ( e = 1. (Polynom-Ring (n,L)) implies ( x * e = x & e * x = x ) )
reconsider p = x as Polynomial of n,L by Def10;
assume A1: e = 1. (Polynom-Ring (n,L)) ; ::_thesis: ( x * e = x & e * x = x )
A2: 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;
hence x * e = p *' (1_ (n,L)) by A1, Def10
.= x by Th29 ;
::_thesis: e * x = x
thus e * x = (1_ (n,L)) *' p by A1, A2, Def10
.= x by Th30 ; ::_thesis: verum
end;
registration
let n be Ordinal;
let L be non empty non trivial right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring (n,L) -> non empty strict right-distributive well-unital ;
coherence
( Polynom-Ring (n,L) is well-unital & Polynom-Ring (n,L) is right-distributive )
proof
set Pm = Polynom-Ring (n,L);
thus Polynom-Ring (n,L) is well-unital ::_thesis: Polynom-Ring (n,L) is right-distributive
proof
let x be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (Polynom-Ring (n,L))) = x & (1. (Polynom-Ring (n,L))) * x = x )
thus ( x * (1. (Polynom-Ring (n,L))) = x & (1. (Polynom-Ring (n,L))) * x = x ) by Lm1; ::_thesis: verum
end;
let x, y, z be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider p = x, q = y, r = z as Polynomial of n,L by Def10;
A1: ( x * y = p *' q & x * z = p *' r ) by Def10;
y + z = q + r by Def10;
hence x * (y + z) = p *' (q + r) by Def10
.= (p *' q) + (p *' r) by Th26
.= (x * y) + (x * z) by A1, Def10 ;
::_thesis: verum
end;
end;
theorem :: POLYNOM1:31
for n being Ordinal
for L being non empty non trivial right_complementable associative right_unital distributive Abelian add-associative right_zeroed doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def10;