:: POLYALG1 semantic presentation
begin
definition
let F be 1-sorted ;
attrc2 is strict ;
struct AlgebraStr over F -> doubleLoopStr , VectSpStr over F;
aggrAlgebraStr(# carrier, addF, multF, ZeroF, OneF, lmult #) -> AlgebraStr over F;
end;
registration
let L be non empty doubleLoopStr ;
cluster non empty strict for AlgebraStr over L;
existence
ex b1 being AlgebraStr over L st
( b1 is strict & not b1 is empty )
proof
0 in {0} by TARSKI:def_1;
then reconsider lm = [: the carrier of L,{0}:] --> 0 as Function of [: the carrier of L,{0}:],{0} by FUNCOP_1:45;
reconsider z = 0 as Element of {0} by TARSKI:def_1;
set a = the BinOp of {0};
take AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) ; ::_thesis: ( AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is strict & not AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is empty )
thus ( AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is strict & not AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) is empty ) ; ::_thesis: verum
end;
end;
definition
let L be non empty doubleLoopStr ;
let A be non empty AlgebraStr over L;
attrA is mix-associative means :: POLYALG1:def 1
for a being Element of L
for x, y being Element of A holds a * (x * y) = (a * x) * y;
end;
:: deftheorem defines mix-associative POLYALG1:def_1_:_
for L being non empty doubleLoopStr
for A being non empty AlgebraStr over L holds
( A is mix-associative iff for a being Element of L
for x, y being Element of A holds a * (x * y) = (a * x) * y );
registration
let L be non empty doubleLoopStr ;
cluster non empty unital distributive vector-distributive scalar-distributive scalar-associative scalar-unital mix-associative for AlgebraStr over L;
existence
ex b1 being non empty AlgebraStr over L st
( b1 is unital & b1 is distributive & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is mix-associative )
proof
0 in {0} by TARSKI:def_1;
then reconsider lm = [: the carrier of L,{0}:] --> 0 as Function of [: the carrier of L,{0}:],{0} by FUNCOP_1:45;
reconsider z = 0 as Element of {0} by TARSKI:def_1;
set a = the BinOp of {0};
reconsider A = AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) as non empty AlgebraStr over L ;
take A ; ::_thesis: ( A is unital & A is distributive & A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
A1: for x, y being Element of A holds x = y
proof
let x, y be Element of A; ::_thesis: x = y
x = 0 by TARSKI:def_1;
hence x = y by TARSKI:def_1; ::_thesis: verum
end;
thus A is unital ::_thesis: ( A is distributive & A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
proof
take 1. A ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of A holds
( b1 * (1. A) = b1 & (1. A) * b1 = b1 )
thus for b1 being Element of the carrier of A holds
( b1 * (1. A) = b1 & (1. A) * b1 = b1 ) by A1; ::_thesis: verum
end;
thus A is distributive ::_thesis: ( A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
proof
let x, y, z be Element of A; :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by A1; ::_thesis: verum
end;
thus A is vector-distributive ::_thesis: ( A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
proof
let x be Element of L; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of A holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of A; ::_thesis: x * (v + w) = (x * v) + (x * w)
thus x * (v + w) = (x * v) + (x * w) by A1; ::_thesis: verum
end;
thus A is scalar-distributive ::_thesis: ( A is scalar-associative & A is scalar-unital & A is mix-associative )
proof
let x, y be Element of L; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of A holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of A; ::_thesis: (x + y) * v = (x * v) + (y * v)
thus (x + y) * v = (x * v) + (y * v) by A1; ::_thesis: verum
end;
thus A is scalar-associative ::_thesis: ( A is scalar-unital & A is mix-associative )
proof
let x, y be Element of L; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of A holds (x * y) * b1 = x * (y * b1)
thus for b1 being Element of the carrier of A holds (x * y) * b1 = x * (y * b1) by A1; ::_thesis: verum
end;
thus A is scalar-unital ::_thesis: A is mix-associative
proof
let v be Element of A; :: according to VECTSP_1:def_17 ::_thesis: (1. L) * v = v
thus (1. L) * v = v by A1; ::_thesis: verum
end;
thus A is mix-associative ::_thesis: verum
proof
let a be Element of L; :: according to POLYALG1:def_1 ::_thesis: for x, y being Element of A holds a * (x * y) = (a * x) * y
let x, y be Element of A; ::_thesis: a * (x * y) = (a * x) * y
thus a * (x * y) = (a * x) * y by A1; ::_thesis: verum
end;
end;
end;
definition
let L be non empty doubleLoopStr ;
mode Algebra of L is non empty unital distributive vector-distributive scalar-distributive scalar-associative scalar-unital mix-associative AlgebraStr over L;
end;
theorem Th1: :: POLYALG1:1
for X, Y being set
for f being Function of [:X,Y:],X holds dom f = [:X,Y:]
proof
let X, Y be set ; ::_thesis: for f being Function of [:X,Y:],X holds dom f = [:X,Y:]
let f be Function of [:X,Y:],X; ::_thesis: dom f = [:X,Y:]
( X is empty implies [:X,Y:] is empty ) by ZFMISC_1:90;
hence dom f = [:X,Y:] by FUNCT_2:def_1; ::_thesis: verum
end;
theorem Th2: :: POLYALG1:2
for X, Y being set
for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
proof
let X, Y be set ; ::_thesis: for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
let f be Function of [:X,Y:],Y; ::_thesis: dom f = [:X,Y:]
( Y is empty implies [:X,Y:] is empty ) by ZFMISC_1:90;
hence dom f = [:X,Y:] by FUNCT_2:def_1; ::_thesis: verum
end;
begin
definition
let L be non empty doubleLoopStr ;
func Formal-Series L -> non empty strict AlgebraStr over L means :Def2: :: POLYALG1:def 2
( ( for x being set holds
( x in the carrier of it iff x is sequence of L ) ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of it
for p being sequence of L st x = p holds
a * x = a * p ) & 0. it = 0_. L & 1. it = 1_. L );
existence
ex b1 being non empty strict AlgebraStr over L st
( ( for x being set holds
( x in the carrier of b1 iff x is sequence of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
proof
A1: 0_. L in { x where x is sequence of L : verum } ;
then reconsider Ca = { x where x is sequence of L : verum } as non empty set ;
reconsider Ze = 0_. L as Element of Ca by A1;
defpred S1[ set , set , set ] means ex p, q being sequence of L st
( p = $1 & q = $2 & $3 = p + q );
A2: for x, y being Element of Ca ex u being Element of Ca st S1[x,y,u]
proof
let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S1[x,y,u]
x in Ca ;
then consider p being sequence of L such that
A3: x = p ;
y in Ca ;
then consider q being sequence of L such that
A4: y = q ;
p + q in Ca ;
then reconsider u = p + q as Element of Ca ;
take u ; ::_thesis: S1[x,y,u]
take p ; ::_thesis: ex q being sequence of L st
( p = x & q = y & u = p + q )
take q ; ::_thesis: ( p = x & q = y & u = p + q )
thus ( p = x & q = y & u = p + q ) by A3, A4; ::_thesis: verum
end;
consider Ad being Function of [:Ca,Ca:],Ca such that
A5: for x, y being Element of Ca holds S1[x,y,Ad . (x,y)] from BINOP_1:sch_3(A2);
1_. L in { x where x is sequence of L : verum } ;
then reconsider Un = 1_. L as Element of Ca ;
defpred S2[ set , set , set ] means ex p, q being sequence of L st
( p = $1 & q = $2 & $3 = p *' q );
A6: for x, y being Element of Ca ex u being Element of Ca st S2[x,y,u]
proof
let x, y be Element of Ca; ::_thesis: ex u being Element of Ca st S2[x,y,u]
x in Ca ;
then consider p being sequence of L such that
A7: x = p ;
y in Ca ;
then consider q being sequence of L such that
A8: y = q ;
p *' q in Ca ;
then reconsider u = p *' q as Element of Ca ;
take u ; ::_thesis: S2[x,y,u]
take p ; ::_thesis: ex q being sequence of L st
( p = x & q = y & u = p *' q )
take q ; ::_thesis: ( p = x & q = y & u = p *' q )
thus ( p = x & q = y & u = p *' q ) by A7, A8; ::_thesis: verum
end;
consider Mu being Function of [:Ca,Ca:],Ca such that
A9: for x, y being Element of Ca holds S2[x,y,Mu . (x,y)] from BINOP_1:sch_3(A6);
defpred S3[ Element of L, set , set ] means ex p being sequence of L st
( p = $2 & $3 = $1 * p );
A10: for a being Element of L
for x being Element of Ca ex u being Element of Ca st S3[a,x,u]
proof
let a be Element of L; ::_thesis: for x being Element of Ca ex u being Element of Ca st S3[a,x,u]
let x be Element of Ca; ::_thesis: ex u being Element of Ca st S3[a,x,u]
x in Ca ;
then consider q being sequence of L such that
A11: x = q ;
a * q in Ca ;
then reconsider u = a * q as Element of Ca ;
take u ; ::_thesis: S3[a,x,u]
take q ; ::_thesis: ( q = x & u = a * q )
thus ( q = x & u = a * q ) by A11; ::_thesis: verum
end;
consider lm being Function of [: the carrier of L,Ca:],Ca such that
A12: for a being Element of L
for x being Element of Ca holds S3[a,x,lm . (a,x)] from BINOP_1:sch_3(A10);
reconsider P = AlgebraStr(# Ca,Ad,Mu,Ze,Un,lm #) as non empty strict AlgebraStr over L ;
take P ; ::_thesis: ( ( for x being set holds
( x in the carrier of P iff x is sequence of L ) ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )
thus for x being set holds
( x in the carrier of P iff x is sequence of L ) ::_thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )
proof
let x be set ; ::_thesis: ( x in the carrier of P iff x is sequence of L )
thus ( x in the carrier of P implies x is sequence of L ) ::_thesis: ( x is sequence of L implies x in the carrier of P )
proof
assume x in the carrier of P ; ::_thesis: x is sequence of L
then ex p being sequence of L st x = p ;
hence x is sequence of L ; ::_thesis: verum
end;
thus ( x is sequence of L implies x in the carrier of P ) ; ::_thesis: verum
end;
thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ::_thesis: ( ( for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )
proof
let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds
x + y = p + q
let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x + y = p + q )
assume A13: ( x = p & y = q ) ; ::_thesis: x + y = p + q
ex p1, q1 being sequence of L st
( p1 = x & q1 = y & Ad . (x,y) = p1 + q1 ) by A5;
hence x + y = p + q by A13; ::_thesis: verum
end;
thus for x, y being Element of P
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ::_thesis: ( ( for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P = 0_. L & 1. P = 1_. L )
proof
let x, y be Element of P; ::_thesis: for p, q being sequence of L st x = p & y = q holds
x * y = p *' q
let p, q be sequence of L; ::_thesis: ( x = p & y = q implies x * y = p *' q )
assume A14: ( x = p & y = q ) ; ::_thesis: x * y = p *' q
ex p1, q1 being sequence of L st
( p1 = x & q1 = y & Mu . (x,y) = p1 *' q1 ) by A9;
hence x * y = p *' q by A14; ::_thesis: verum
end;
thus for a being Element of L
for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p ::_thesis: ( 0. P = 0_. L & 1. P = 1_. L )
proof
let a be Element of L; ::_thesis: for x being Element of P
for p being sequence of L st x = p holds
a * x = a * p
let x be Element of P; ::_thesis: for p being sequence of L st x = p holds
a * x = a * p
let p be sequence of L; ::_thesis: ( x = p implies a * x = a * p )
assume A15: x = p ; ::_thesis: a * x = a * p
ex p1 being sequence of L st
( x = p1 & lm . (a,x) = a * p1 ) by A12;
hence a * x = a * p by A15; ::_thesis: verum
end;
thus 0. P = 0_. L ; ::_thesis: 1. P = 1_. L
thus 1. P = 1_. L ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict AlgebraStr over L st ( for x being set holds
( x in the carrier of b1 iff x is sequence of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is sequence of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b2
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
proof
let P1, P2 be non empty strict AlgebraStr over L; ::_thesis: ( ( for x being set holds
( x in the carrier of P1 iff x is sequence of L ) ) & ( for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P1 = 0_. L & 1. P1 = 1_. L & ( for x being set holds
( x in the carrier of P2 iff x is sequence of L ) ) & ( for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of P2
for p being sequence of L st x = p holds
a * x = a * p ) & 0. P2 = 0_. L & 1. P2 = 1_. L implies P1 = P2 )
assume that
A16: for x being set holds
( x in the carrier of P1 iff x is sequence of L ) and
A17: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A18: for x, y being Element of P1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A19: for a being Element of L
for x being Element of P1
for p being sequence of L st x = p holds
a * x = a * p and
A20: ( 0. P1 = 0_. L & 1. P1 = 1_. L ) and
A21: for x being set holds
( x in the carrier of P2 iff x is sequence of L ) and
A22: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q and
A23: for x, y being Element of P2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q and
A24: for a being Element of L
for x being Element of P2
for p being sequence of L st x = p holds
a * x = a * p and
A25: ( 0. P2 = 0_. L & 1. P2 = 1_. L ) ; ::_thesis: P1 = P2
A26: now__::_thesis:_for_x_being_set_holds_
(_x_in_the_carrier_of_P1_iff_x_in_the_carrier_of_P2_)
let x be set ; ::_thesis: ( x in the carrier of P1 iff x in the carrier of P2 )
( x in the carrier of P1 iff x is sequence of L ) by A16;
hence ( x in the carrier of P1 iff x in the carrier of P2 ) by A21; ::_thesis: verum
end;
then A27: the carrier of P1 = the carrier of P2 by TARSKI:1;
now__::_thesis:_for_a_being_Element_of_L
for_x_being_Element_of_P1_holds_the_lmult_of_P1_._(a,x)_=_the_lmult_of_P2_._(a,x)
let a be Element of L; ::_thesis: for x being Element of P1 holds the lmult of P1 . (a,x) = the lmult of P2 . (a,x)
let x be Element of P1; ::_thesis: the lmult of P1 . (a,x) = the lmult of P2 . (a,x)
reconsider p = x as sequence of L by A16;
reconsider x1 = x as Element of P2 by A26;
reconsider a1 = a as Element of L ;
thus the lmult of P1 . (a,x) = a * x
.= a1 * p by A19
.= a1 * x1 by A24
.= the lmult of P2 . (a,x) ; ::_thesis: verum
end;
then A28: the lmult of P1 = the lmult of P2 by A27, BINOP_1:2;
A29: now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_multF_of_P1_._(x,y)_=_the_multF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)
let y be Element of P2; ::_thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A26;
reconsider x1 = x as Element of P2 by A26;
reconsider p = x as sequence of L by A16;
reconsider q = y as sequence of L by A21;
thus the multF of P1 . (x,y) = x * y1
.= p *' q by A18
.= x1 * y by A23
.= the multF of P2 . (x,y) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_addF_of_P1_._(x,y)_=_the_addF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)
let y be Element of P2; ::_thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A26;
reconsider x1 = x as Element of P2 by A26;
reconsider p = x as sequence of L by A16;
reconsider q = y as sequence of L by A21;
thus the addF of P1 . (x,y) = x + y1
.= p + q by A17
.= x1 + y by A22
.= the addF of P2 . (x,y) ; ::_thesis: verum
end;
then the addF of P1 = the addF of P2 by A27, BINOP_1:2;
hence P1 = P2 by A20, A25, A27, A29, A28, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Formal-Series POLYALG1:def_2_:_
for L being non empty doubleLoopStr
for b2 being non empty strict AlgebraStr over L holds
( b2 = Formal-Series L iff ( ( for x being set holds
( x in the carrier of b2 iff x is sequence of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b2
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b2 = 0_. L & 1. b2 = 1_. L ) );
registration
let L be non empty Abelian doubleLoopStr ;
cluster Formal-Series L -> non empty Abelian strict ;
coherence
Formal-Series L is Abelian
proof
let p, q be Element of (Formal-Series L); :: according to RLVECT_1:def_2 ::_thesis: p + q = q + p
reconsider p1 = p, q1 = q as sequence of L by Def2;
thus p + q = p1 + q1 by Def2
.= q + p by Def2 ; ::_thesis: verum
end;
end;
registration
let L be non empty add-associative doubleLoopStr ;
cluster Formal-Series L -> non empty add-associative strict ;
coherence
Formal-Series L is add-associative
proof
let p, q, r be Element of (Formal-Series L); :: according to RLVECT_1:def_3 ::_thesis: (p + q) + r = p + (q + r)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;
A1: q + r = q1 + r1 by Def2;
p + q = p1 + q1 by Def2;
hence (p + q) + r = (p1 + q1) + r1 by Def2
.= p1 + (q1 + r1) by POLYNOM3:26
.= p + (q + r) by A1, Def2 ;
::_thesis: verum
end;
end;
registration
let L be non empty right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty right_zeroed strict ;
coherence
Formal-Series L is right_zeroed
proof
let p be Element of (Formal-Series L); :: according to RLVECT_1:def_4 ::_thesis: p + (0. (Formal-Series L)) = p
reconsider p1 = p as sequence of L by Def2;
0. (Formal-Series L) = 0_. L by Def2;
hence p + (0. (Formal-Series L)) = p1 + (0_. L) by Def2
.= p by POLYNOM3:28 ;
::_thesis: verum
end;
end;
registration
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty right_complementable strict ;
coherence
Formal-Series L is right_complementable
proof
let p be Element of (Formal-Series L); :: according to ALGSTR_0:def_16 ::_thesis: p is right_complementable
reconsider p1 = p as sequence of L by Def2;
reconsider q = - p1 as Element of (Formal-Series L) by Def2;
take q ; :: according to ALGSTR_0:def_11 ::_thesis: p + q = 0. (Formal-Series L)
thus p + q = p1 + (- p1) by Def2
.= p1 - p1 by POLYNOM3:def_6
.= 0_. L by POLYNOM3:29
.= 0. (Formal-Series L) by Def2 ; ::_thesis: verum
end;
end;
registration
let L be non empty commutative Abelian add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty commutative strict ;
coherence
Formal-Series L is commutative
proof
let p, q be Element of (Formal-Series L); :: according to GROUP_1:def_12 ::_thesis: p * q = q * p
reconsider p1 = p, q1 = q as sequence of L by Def2;
thus p * q = p1 *' q1 by Def2
.= q * p by Def2 ; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty associative strict ;
coherence
Formal-Series L is associative
proof
let p, q, r be Element of (Formal-Series L); :: according to GROUP_1:def_3 ::_thesis: (p * q) * r = p * (q * r)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;
A1: q * r = q1 *' r1 by Def2;
p * q = p1 *' q1 by Def2;
hence (p * q) * r = (p1 *' q1) *' r1 by Def2
.= p1 *' (q1 *' r1) by POLYNOM3:33
.= p * (q * r) by A1, Def2 ;
::_thesis: verum
end;
end;
registration
cluster non empty right_complementable left_zeroed associative well-unital distributive add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is add-associative & b1 is associative & b1 is right_zeroed & b1 is left_zeroed & b1 is well-unital & b1 is right_complementable & b1 is distributive )
proof
take F_Real ; ::_thesis: ( F_Real is add-associative & F_Real is associative & F_Real is right_zeroed & F_Real is left_zeroed & F_Real is well-unital & F_Real is right_complementable & F_Real is distributive )
thus ( F_Real is add-associative & F_Real is associative & F_Real is right_zeroed & F_Real is left_zeroed & F_Real is well-unital & F_Real is right_complementable & F_Real is distributive ) ; ::_thesis: verum
end;
end;
theorem Th3: :: POLYALG1:3
for D being non empty set
for f being non empty FinSequence of D holds f /^ 1 = Del (f,1)
proof
let D be non empty set ; ::_thesis: for f being non empty FinSequence of D holds f /^ 1 = Del (f,1)
let f be non empty FinSequence of D; ::_thesis: f /^ 1 = Del (f,1)
consider i being Nat such that
A1: i + 1 = len f by FINSEQ_5:7;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A2: 1 <= len f by A1, NAT_1:11;
( len (f /^ 1) = len (Del (f,1)) & ( for k being Nat st 1 <= k & k <= len (f /^ 1) holds
(f /^ 1) . k = (Del (f,1)) . k ) )
proof
A3: len (f /^ 1) = (i + 1) - 1 by A1, A2, RFINSEQ:def_1
.= i ;
1 in dom f by FINSEQ_5:6;
hence len (f /^ 1) = len (Del (f,1)) by A1, A3, FINSEQ_3:109; ::_thesis: for k being Nat st 1 <= k & k <= len (f /^ 1) holds
(f /^ 1) . k = (Del (f,1)) . k
A4: 1 in dom f by FINSEQ_5:6;
let k be Nat; ::_thesis: ( 1 <= k & k <= len (f /^ 1) implies (f /^ 1) . k = (Del (f,1)) . k )
assume A5: ( 1 <= k & k <= len (f /^ 1) ) ; ::_thesis: (f /^ 1) . k = (Del (f,1)) . k
k in dom (f /^ 1) by A5, FINSEQ_3:25;
hence (f /^ 1) . k = f . (k + 1) by A2, RFINSEQ:def_1
.= (Del (f,1)) . k by A1, A3, A5, A4, FINSEQ_3:111 ;
::_thesis: verum
end;
hence f /^ 1 = Del (f,1) by FINSEQ_1:14; ::_thesis: verum
end;
theorem Th4: :: POLYALG1:4
for D being non empty set
for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))
proof
let D be non empty set ; ::_thesis: for f being non empty FinSequence of D holds f = <*(f . 1)*> ^ (Del (f,1))
let f be non empty FinSequence of D; ::_thesis: f = <*(f . 1)*> ^ (Del (f,1))
A1: 1 in dom f by FINSEQ_5:6;
thus f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29
.= <*(f . 1)*> ^ (f /^ 1) by A1, PARTFUN1:def_6
.= <*(f . 1)*> ^ (Del (f,1)) by Th3 ; ::_thesis: verum
end;
theorem Th5: :: POLYALG1:5
for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p
proof
let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for p being sequence of L holds (1_. L) *' p = p
let p be sequence of L; ::_thesis: (1_. L) *' p = p
now__::_thesis:_for_i_being_Element_of_NAT_holds_((1_._L)_*'_p)_._i_=_p_._i
let i be Element of NAT ; ::_thesis: ((1_. L) *' p) . i = p . i
consider r being FinSequence of the carrier of L such that
A1: len r = i + 1 and
A2: ((1_. L) *' p) . i = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = ((1_. L) . (k -' 1)) * (p . ((i + 1) -' k)) by POLYNOM3:def_9;
A4: 1 in dom r by A1, CARD_1:27, FINSEQ_5:6;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(Del_(r,1))_holds_
(Del_(r,1))_._k_=_0._L
let k be Element of NAT ; ::_thesis: ( k in dom (Del (r,1)) implies (Del (r,1)) . k = 0. L )
A5: k + 1 >= 1 by NAT_1:11;
assume A6: k in dom (Del (r,1)) ; ::_thesis: (Del (r,1)) . k = 0. L
then A7: k <> 0 by FINSEQ_3:25;
len (Del (r,1)) = i by A1, A4, FINSEQ_3:109;
then A8: k <= i by A6, FINSEQ_3:25;
then k + 1 <= i + 1 by XREAL_1:6;
then A9: k + 1 in dom r by A1, A5, FINSEQ_3:25;
0 + 1 <= k by A6, FINSEQ_3:25;
hence (Del (r,1)) . k = r . (k + 1) by A1, A4, A8, FINSEQ_3:111
.= ((1_. L) . ((k + 1) -' 1)) * (p . ((i + 1) -' (k + 1))) by A3, A9
.= ((1_. L) . k) * (p . ((i + 1) -' (k + 1))) by NAT_D:34
.= (0. L) * (p . ((i + 1) -' (k + 1))) by A7, POLYNOM3:30
.= 0. L by VECTSP_1:7 ;
::_thesis: verum
end;
then A10: Sum (Del (r,1)) = 0. L by POLYNOM3:1;
r = <*(r . 1)*> ^ (Del (r,1)) by A1, Th4, CARD_1:27
.= <*(r /. 1)*> ^ (Del (r,1)) by A4, PARTFUN1:def_6 ;
then A11: Sum r = (Sum <*(r /. 1)*>) + (Sum (Del (r,1))) by RLVECT_1:41
.= (r /. 1) + (Sum (Del (r,1))) by RLVECT_1:44 ;
r /. 1 = r . 1 by A4, PARTFUN1:def_6
.= ((1_. L) . (1 -' 1)) * (p . ((i + 1) -' 1)) by A3, A4
.= ((1_. L) . (1 -' 1)) * (p . i) by NAT_D:34
.= ((1_. L) . 0) * (p . i) by XREAL_1:232
.= (1_ L) * (p . i) by POLYNOM3:30
.= p . i by VECTSP_1:def_8 ;
hence ((1_. L) *' p) . i = p . i by A2, A11, A10, RLVECT_1:4; ::_thesis: verum
end;
hence (1_. L) *' p = p by FUNCT_2:63; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_L_being_non_empty_right_complementable_well-unital_distributive_add-associative_right_zeroed_doubleLoopStr_
for_x,_e_being_Element_of_(Formal-Series_L)_st_e_=_1_._L_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, e being Element of (Formal-Series L) st e = 1_. L holds
( x * e = x & e * x = x )
set F = Formal-Series L;
let x, e be Element of (Formal-Series L); ::_thesis: ( e = 1_. L implies ( x * e = x & e * x = x ) )
reconsider a = x, b = e as sequence of L by Def2;
assume A1: e = 1_. L ; ::_thesis: ( x * e = x & e * x = x )
thus x * e = a *' b by Def2
.= x by A1, POLYNOM3:35 ; ::_thesis: e * x = x
thus e * x = b *' a by Def2
.= x by A1, Th5 ; ::_thesis: verum
end;
registration
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty well-unital strict ;
coherence
Formal-Series L is well-unital
proof
let x be Element of (Formal-Series L); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (Formal-Series L)) = x & (1. (Formal-Series L)) * x = x )
set F = Formal-Series L;
1. (Formal-Series L) = 1_. L by Def2;
hence ( x * (1. (Formal-Series L)) = x & (1. (Formal-Series L)) * x = x ) by Lm1; ::_thesis: verum
end;
end;
registration
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty right-distributive strict ;
coherence
Formal-Series L is right-distributive
proof
let p, q, r be Element of (Formal-Series L); :: according to VECTSP_1:def_2 ::_thesis: p * (q + r) = (p * q) + (p * r)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;
A1: ( p * q = p1 *' q1 & p * r = p1 *' r1 ) by Def2;
q + r = q1 + r1 by Def2;
hence p * (q + r) = p1 *' (q1 + r1) by Def2
.= (p1 *' q1) + (p1 *' r1) by POLYNOM3:31
.= (p * q) + (p * r) by A1, Def2 ;
::_thesis: verum
end;
cluster Formal-Series L -> non empty left-distributive strict ;
coherence
Formal-Series L is left-distributive
proof
let p, q, r be Element of (Formal-Series L); :: according to VECTSP_1:def_3 ::_thesis: (q + r) * p = (q * p) + (r * p)
reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;
A2: ( q * p = q1 *' p1 & r * p = r1 *' p1 ) by Def2;
q + r = q1 + r1 by Def2;
hence (q + r) * p = (q1 + r1) *' p1 by Def2
.= (q1 *' p1) + (r1 *' p1) by POLYNOM3:32
.= (q * p) + (r * p) by A2, Def2 ;
::_thesis: verum
end;
end;
theorem Th6: :: POLYALG1:6
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of L
for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)
proof
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L
for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)
let a be Element of L; ::_thesis: for p, q being sequence of L holds a * (p + q) = (a * p) + (a * q)
let p, q be sequence of L; ::_thesis: a * (p + q) = (a * p) + (a * q)
for i being Element of NAT holds (a * (p + q)) . i = ((a * p) + (a * q)) . i
proof
let i be Element of NAT ; ::_thesis: (a * (p + q)) . i = ((a * p) + (a * q)) . i
a * ((p + q) . i) = a * ((p . i) + (q . i)) by NORMSP_1:def_2
.= (a * (p . i)) + (a * (q . i)) by VECTSP_1:def_7
.= ((a * p) . i) + (a * (q . i)) by POLYNOM5:def_3
.= ((a * p) . i) + ((a * q) . i) by POLYNOM5:def_3
.= ((a * p) + (a * q)) . i by NORMSP_1:def_2 ;
hence (a * (p + q)) . i = ((a * p) + (a * q)) . i by POLYNOM5:def_3; ::_thesis: verum
end;
hence a * (p + q) = (a * p) + (a * q) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th7: :: POLYALG1:7
for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for a, b being Element of L
for p being sequence of L holds (a + b) * p = (a * p) + (b * p)
proof
let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of L
for p being sequence of L holds (a + b) * p = (a * p) + (b * p)
let a, b be Element of L; ::_thesis: for p being sequence of L holds (a + b) * p = (a * p) + (b * p)
let p be sequence of L; ::_thesis: (a + b) * p = (a * p) + (b * p)
for i being Element of NAT holds ((a + b) * p) . i = ((a * p) + (b * p)) . i
proof
let i be Element of NAT ; ::_thesis: ((a + b) * p) . i = ((a * p) + (b * p)) . i
thus ((a + b) * p) . i = (a + b) * (p . i) by POLYNOM5:def_3
.= (a * (p . i)) + (b * (p . i)) by VECTSP_1:def_7
.= ((a * p) . i) + (b * (p . i)) by POLYNOM5:def_3
.= ((a * p) . i) + ((b * p) . i) by POLYNOM5:def_3
.= ((a * p) + (b * p)) . i by NORMSP_1:def_2 ; ::_thesis: verum
end;
hence (a + b) * p = (a * p) + (b * p) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th8: :: POLYALG1:8
for L being non empty associative doubleLoopStr
for a, b being Element of L
for p being sequence of L holds (a * b) * p = a * (b * p)
proof
let L be non empty associative doubleLoopStr ; ::_thesis: for a, b being Element of L
for p being sequence of L holds (a * b) * p = a * (b * p)
let a, b be Element of L; ::_thesis: for p being sequence of L holds (a * b) * p = a * (b * p)
let p be sequence of L; ::_thesis: (a * b) * p = a * (b * p)
for i being Element of NAT holds ((a * b) * p) . i = (a * (b * p)) . i
proof
let i be Element of NAT ; ::_thesis: ((a * b) * p) . i = (a * (b * p)) . i
thus ((a * b) * p) . i = (a * b) * (p . i) by POLYNOM5:def_3
.= a * (b * (p . i)) by GROUP_1:def_3
.= a * ((b * p) . i) by POLYNOM5:def_3
.= (a * (b * p)) . i by POLYNOM5:def_3 ; ::_thesis: verum
end;
hence (a * b) * p = a * (b * p) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th9: :: POLYALG1:9
for L being non empty associative well-unital doubleLoopStr
for p being sequence of L holds (1. L) * p = p
proof
let L be non empty associative well-unital doubleLoopStr ; ::_thesis: for p being sequence of L holds (1. L) * p = p
let p be sequence of L; ::_thesis: (1. L) * p = p
for i being Element of NAT holds ((1. L) * p) . i = p . i
proof
let i be Element of NAT ; ::_thesis: ((1. L) * p) . i = p . i
thus ((1. L) * p) . i = (1. L) * (p . i) by POLYNOM5:def_3
.= p . i by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence (1. L) * p = p by FUNCT_2:63; ::_thesis: verum
end;
registration
let L be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty vector-distributive scalar-distributive scalar-associative scalar-unital strict ;
coherence
( Formal-Series L is vector-distributive & Formal-Series L is scalar-distributive & Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )
proof
set F = Formal-Series L;
thus Formal-Series L is vector-distributive ::_thesis: ( Formal-Series L is scalar-distributive & Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )
proof
let x be Element of L; :: according to VECTSP_1:def_14 ::_thesis: for b1, b2 being Element of the carrier of (Formal-Series L) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of (Formal-Series L); ::_thesis: x * (v + w) = (x * v) + (x * w)
reconsider p = v, q = w as sequence of L by Def2;
reconsider x9 = x as Element of L ;
reconsider k = v + w as Element of (Formal-Series L) ;
A1: x * v = x * p by Def2;
reconsider r = k as sequence of L by Def2;
A2: x * w = x * q by Def2;
x * k = x * r by Def2;
hence x * (v + w) = x * (p + q) by Def2
.= (x9 * p) + (x9 * q) by Th6
.= (x * v) + (x * w) by A1, A2, Def2 ;
::_thesis: verum
end;
thus Formal-Series L is scalar-distributive ::_thesis: ( Formal-Series L is scalar-associative & Formal-Series L is scalar-unital )
proof
let x, y be Element of L; :: according to VECTSP_1:def_15 ::_thesis: for b1 being Element of the carrier of (Formal-Series L) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of (Formal-Series L); ::_thesis: (x + y) * v = (x * v) + (y * v)
reconsider p = v as sequence of L by Def2;
reconsider x9 = x, y9 = y as Element of L ;
A3: x * v = x * p by Def2;
A4: y * v = y * p by Def2;
thus (x + y) * v = (x9 + y9) * p by Def2
.= (x9 * p) + (y9 * p) by Th7
.= (x * v) + (y * v) by A3, A4, Def2 ; ::_thesis: verum
end;
thus Formal-Series L is scalar-associative ::_thesis: Formal-Series L is scalar-unital
proof
let x, y be Element of L; :: according to VECTSP_1:def_16 ::_thesis: for b1 being Element of the carrier of (Formal-Series L) holds (x * y) * b1 = x * (y * b1)
let v be Element of (Formal-Series L); ::_thesis: (x * y) * v = x * (y * v)
reconsider p = v as sequence of L by Def2;
reconsider x9 = x, y9 = y as Element of L ;
A5: y * v = y * p by Def2;
thus (x * y) * v = (x9 * y9) * p by Def2
.= x9 * (y9 * p) by Th8
.= x * (y * v) by A5, Def2 ; ::_thesis: verum
end;
let v be Element of (Formal-Series L); :: according to VECTSP_1:def_17 ::_thesis: (1. L) * v = v
reconsider p = v as sequence of L by Def2;
thus (1. L) * v = (1. L) * p by Def2
.= v by Th9 ; ::_thesis: verum
end;
end;
theorem Th10: :: POLYALG1:10
for L being non empty right_complementable left_zeroed associative distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of L
for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
proof
let L be non empty right_complementable left_zeroed associative distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a being Element of L
for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
let a be Element of L; ::_thesis: for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
let p, q be sequence of L; ::_thesis: a * (p *' q) = (a * p) *' q
for x being Element of NAT holds (a * (p *' q)) . x = ((a * p) *' q) . x
proof
let i be Element of NAT ; ::_thesis: (a * (p *' q)) . i = ((a * p) *' q) . i
consider f1 being FinSequence of the carrier of L such that
A1: len f1 = i + 1 and
A2: (p *' q) . i = Sum f1 and
A3: for k being Element of NAT st k in dom f1 holds
f1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def_9;
consider f2 being FinSequence of the carrier of L such that
A4: len f2 = i + 1 and
A5: ((a * p) *' q) . i = Sum f2 and
A6: for k being Element of NAT st k in dom f2 holds
f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def_9;
A7: dom (a * f1) = dom f1 by POLYNOM1:def_1
.= dom f2 by A1, A4, FINSEQ_3:29 ;
A8: for k being Nat st k in dom f2 holds
f2 . k = (a * f1) . k
proof
let k be Nat; ::_thesis: ( k in dom f2 implies f2 . k = (a * f1) . k )
assume A9: k in dom f2 ; ::_thesis: f2 . k = (a * f1) . k
A10: k in dom f1 by A1, A4, A9, FINSEQ_3:29;
then A11: (p . (k -' 1)) * (q . ((i + 1) -' k)) = f1 . k by A3
.= f1 /. k by A10, PARTFUN1:def_6 ;
thus f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by A6, A9
.= (a * (p . (k -' 1))) * (q . ((i + 1) -' k)) by POLYNOM5:def_3
.= a * (f1 /. k) by A11, GROUP_1:def_3
.= (a * f1) /. k by A10, POLYNOM1:def_1
.= (a * f1) . k by A7, A9, PARTFUN1:def_6 ; ::_thesis: verum
end;
thus (a * (p *' q)) . i = a * (Sum f1) by A2, POLYNOM5:def_3
.= Sum (a * f1) by BINOM:4
.= ((a * p) *' q) . i by A5, A7, A8, FINSEQ_1:13 ; ::_thesis: verum
end;
hence a * (p *' q) = (a * p) *' q by FUNCT_2:63; ::_thesis: verum
end;
registration
let L be non empty right_complementable left_zeroed associative distributive Abelian add-associative right_zeroed doubleLoopStr ;
cluster Formal-Series L -> non empty strict mix-associative ;
coherence
Formal-Series L is mix-associative
proof
let a be Element of L; :: according to POLYALG1:def_1 ::_thesis: for x, y being Element of (Formal-Series L) holds a * (x * y) = (a * x) * y
let x, y be Element of (Formal-Series L); ::_thesis: a * (x * y) = (a * x) * y
reconsider x1 = x, y1 = y as Element of (Formal-Series L) ;
reconsider p = x1, q = y1 as sequence of L by Def2;
A1: a * x = a * p by Def2;
x * y = p *' q by Def2;
hence a * (x * y) = a * (p *' q) by Def2
.= (a * p) *' q by Th10
.= (a * x) * y by A1, Def2 ;
::_thesis: verum
end;
end;
definition
let L be 1-sorted ;
let A be AlgebraStr over L;
mode Subalgebra of A -> AlgebraStr over L means :Def3: :: POLYALG1:def 3
( the carrier of it c= the carrier of A & 1. it = 1. A & 0. it = 0. A & the addF of it = the addF of A || the carrier of it & the multF of it = the multF of A || the carrier of it & the lmult of it = the lmult of A | [: the carrier of L, the carrier of it:] );
existence
ex b1 being AlgebraStr over L st
( the carrier of b1 c= the carrier of A & 1. b1 = 1. A & 0. b1 = 0. A & the addF of b1 = the addF of A || the carrier of b1 & the multF of b1 = the multF of A || the carrier of b1 & the lmult of b1 = the lmult of A | [: the carrier of L, the carrier of b1:] )
proof
take A ; ::_thesis: ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] )
thus ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] ) ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Subalgebra POLYALG1:def_3_:_
for L being 1-sorted
for A, b3 being AlgebraStr over L holds
( b3 is Subalgebra of A iff ( the carrier of b3 c= the carrier of A & 1. b3 = 1. A & 0. b3 = 0. A & the addF of b3 = the addF of A || the carrier of b3 & the multF of b3 = the multF of A || the carrier of b3 & the lmult of b3 = the lmult of A | [: the carrier of L, the carrier of b3:] ) );
theorem Th11: :: POLYALG1:11
for L being 1-sorted
for A being AlgebraStr over L holds A is Subalgebra of A
proof
let L be 1-sorted ; ::_thesis: for A being AlgebraStr over L holds A is Subalgebra of A
let A be AlgebraStr over L; ::_thesis: A is Subalgebra of A
thus ( the carrier of A c= the carrier of A & 1. A = 1. A & 0. A = 0. A & the addF of A = the addF of A || the carrier of A & the multF of A = the multF of A || the carrier of A & the lmult of A = the lmult of A | [: the carrier of L, the carrier of A:] ) ; :: according to POLYALG1:def_3 ::_thesis: verum
end;
theorem :: POLYALG1:12
for L being 1-sorted
for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds
A is Subalgebra of C
proof
let L be 1-sorted ; ::_thesis: for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds
A is Subalgebra of C
let A, B, C be AlgebraStr over L; ::_thesis: ( A is Subalgebra of B & B is Subalgebra of C implies A is Subalgebra of C )
assume that
A1: A is Subalgebra of B and
A2: B is Subalgebra of C ; ::_thesis: A is Subalgebra of C
A3: the carrier of A c= the carrier of B by A1, Def3;
then A4: [: the carrier of A, the carrier of A:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;
the carrier of B c= the carrier of C by A2, Def3;
hence the carrier of A c= the carrier of C by A3, XBOOLE_1:1; :: according to POLYALG1:def_3 ::_thesis: ( 1. A = 1. C & 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus 1. A = 1. B by A1, Def3
.= 1. C by A2, Def3 ; ::_thesis: ( 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus 0. A = 0. B by A1, Def3
.= 0. C by A2, Def3 ; ::_thesis: ( the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus the addF of A = the addF of B || the carrier of A by A1, Def3
.= ( the addF of C || the carrier of B) || the carrier of A by A2, Def3
.= the addF of C || the carrier of A by A4, FUNCT_1:51 ; ::_thesis: ( the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus the multF of A = the multF of B || the carrier of A by A1, Def3
.= ( the multF of C || the carrier of B) || the carrier of A by A2, Def3
.= the multF of C || the carrier of A by A4, FUNCT_1:51 ; ::_thesis: the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:]
A5: [: the carrier of L, the carrier of A:] c= [: the carrier of L, the carrier of B:] by A3, ZFMISC_1:96;
thus the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] by A1, Def3
.= ( the lmult of C | [: the carrier of L, the carrier of B:]) | [: the carrier of L, the carrier of A:] by A2, Def3
.= the lmult of C | [: the carrier of L, the carrier of A:] by A5, FUNCT_1:51 ; ::_thesis: verum
end;
theorem :: POLYALG1:13
for L being 1-sorted
for A, B being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of A holds
AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #)
proof
let L be 1-sorted ; ::_thesis: for A, B being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of A holds
AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #)
let A, B be AlgebraStr over L; ::_thesis: ( A is Subalgebra of B & B is Subalgebra of A implies AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) )
assume that
A1: A is Subalgebra of B and
A2: B is Subalgebra of A ; ::_thesis: AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #)
A3: the carrier of B c= the carrier of A by A2, Def3;
A4: the carrier of A c= the carrier of B by A1, Def3;
then A5: the carrier of A = the carrier of B by A3, XBOOLE_0:def_10;
A6: dom the lmult of B = [: the carrier of L, the carrier of B:] by Th2;
A7: the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] by A1, Def3
.= the lmult of B by A3, A6, RELAT_1:68, ZFMISC_1:96 ;
A8: dom the addF of B = [: the carrier of B, the carrier of B:] by Th1;
A9: ( 0. A = 0. B & 1. A = 1. B ) by A1, Def3;
A10: dom the multF of B = [: the carrier of B, the carrier of B:] by Th1;
A11: the multF of A = the multF of B || the carrier of A by A1, Def3
.= the multF of B by A5, A10, RELAT_1:68 ;
the addF of A = the addF of B || the carrier of A by A1, Def3
.= the addF of B by A5, A8, RELAT_1:68 ;
hence AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) by A4, A3, A11, A7, A9, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th14: :: POLYALG1:14
for L being 1-sorted
for A, B being AlgebraStr over L st AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) holds
A is Subalgebra of B
proof
let L be 1-sorted ; ::_thesis: for A, B being AlgebraStr over L st AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) holds
A is Subalgebra of B
let A, B be AlgebraStr over L; ::_thesis: ( AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) implies A is Subalgebra of B )
assume A1: AlgebraStr(# the carrier of A, the addF of A, the multF of A, the ZeroF of A, the OneF of A, the lmult of A #) = AlgebraStr(# the carrier of B, the addF of B, the multF of B, the ZeroF of B, the OneF of B, the lmult of B #) ; ::_thesis: A is Subalgebra of B
thus the carrier of A c= the carrier of B by A1; :: according to POLYALG1:def_3 ::_thesis: ( 1. A = 1. B & 0. A = 0. B & the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] )
thus 1. A = 1. B by A1; ::_thesis: ( 0. A = 0. B & the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] )
thus 0. A = 0. B by A1; ::_thesis: ( the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] )
dom the addF of B = [: the carrier of B, the carrier of B:] by Th1;
hence the addF of A = the addF of B || the carrier of A by A1, RELAT_1:68; ::_thesis: ( the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] )
dom the multF of B = [: the carrier of B, the carrier of B:] by Th1;
hence the multF of A = the multF of B || the carrier of A by A1, RELAT_1:68; ::_thesis: the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:]
dom the lmult of B = [: the carrier of L, the carrier of B:] by Th2;
hence the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:] by A1, RELAT_1:68; ::_thesis: verum
end;
registration
let L be non empty 1-sorted ;
cluster non empty strict for AlgebraStr over L;
existence
ex b1 being AlgebraStr over L st
( not b1 is empty & b1 is strict )
proof
0 in {0} by TARSKI:def_1;
then reconsider lm = [: the carrier of L,{0}:] --> 0 as Function of [: the carrier of L,{0}:],{0} by FUNCOP_1:45;
reconsider z = 0 as Element of {0} by TARSKI:def_1;
set A = {0};
set a = the BinOp of {0};
take B = AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #); ::_thesis: ( not B is empty & B is strict )
thus not B is empty ; ::_thesis: B is strict
thus B is strict ; ::_thesis: verum
end;
end;
registration
let L be 1-sorted ;
let B be AlgebraStr over L;
cluster strict for Subalgebra of B;
existence
ex b1 being Subalgebra of B st b1 is strict
proof
reconsider b = AlgebraStr(# the carrier of B, the addF of B, the multF of B,(0. B),(1. B), the lmult of B #) as Subalgebra of B by Th14;
take b ; ::_thesis: b is strict
thus b is strict ; ::_thesis: verum
end;
end;
registration
let L be non empty 1-sorted ;
let B be non empty AlgebraStr over L;
cluster non empty strict for Subalgebra of B;
existence
ex b1 being Subalgebra of B st
( b1 is strict & not b1 is empty )
proof
reconsider b = AlgebraStr(# the carrier of B, the addF of B, the multF of B,(0. B),(1. B), the lmult of B #) as Subalgebra of B by Th14;
take b ; ::_thesis: ( b is strict & not b is empty )
thus ( b is strict & not b is empty ) ; ::_thesis: verum
end;
end;
definition
let L be non empty multMagma ;
let B be non empty AlgebraStr over L;
let A be Subset of B;
attrA is opers_closed means :Def4: :: POLYALG1:def 4
( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds
x * y in A ) & 1. B in A & 0. B in A );
end;
:: deftheorem Def4 defines opers_closed POLYALG1:def_4_:_
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being Subset of B holds
( A is opers_closed iff ( A is linearly-closed & ( for x, y being Element of B st x in A & y in A holds
x * y in A ) & 1. B in A & 0. B in A ) );
theorem Th15: :: POLYALG1:15
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x + y = x9 + y9
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x + y = x9 + y9
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x + y = x9 + y9
let A be non empty Subalgebra of B; ::_thesis: for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x + y = x9 + y9
let x, y be Element of B; ::_thesis: for x9, y9 being Element of A st x = x9 & y = y9 holds
x + y = x9 + y9
let x9, y9 be Element of A; ::_thesis: ( x = x9 & y = y9 implies x + y = x9 + y9 )
assume A1: ( x = x9 & y = y9 ) ; ::_thesis: x + y = x9 + y9
[x9,y9] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
hence x + y = ( the addF of B || the carrier of A) . [x9,y9] by A1, FUNCT_1:49
.= x9 + y9 by Def3 ;
::_thesis: verum
end;
theorem Th16: :: POLYALG1:16
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x * y = x9 * y9
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x * y = x9 * y9
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subalgebra of B
for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x * y = x9 * y9
let A be non empty Subalgebra of B; ::_thesis: for x, y being Element of B
for x9, y9 being Element of A st x = x9 & y = y9 holds
x * y = x9 * y9
let x, y be Element of B; ::_thesis: for x9, y9 being Element of A st x = x9 & y = y9 holds
x * y = x9 * y9
let x9, y9 be Element of A; ::_thesis: ( x = x9 & y = y9 implies x * y = x9 * y9 )
assume A1: ( x = x9 & y = y9 ) ; ::_thesis: x * y = x9 * y9
[x9,y9] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
hence x * y = ( the multF of B || the carrier of A) . [x9,y9] by A1, FUNCT_1:49
.= x9 * y9 by Def3 ;
::_thesis: verum
end;
theorem Th17: :: POLYALG1:17
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let A be non empty Subalgebra of B; ::_thesis: for a being Element of L
for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let a be Element of L; ::_thesis: for x being Element of B
for x9 being Element of A st x = x9 holds
a * x = a * x9
let x be Element of B; ::_thesis: for x9 being Element of A st x = x9 holds
a * x = a * x9
let x9 be Element of A; ::_thesis: ( x = x9 implies a * x = a * x9 )
assume A1: x = x9 ; ::_thesis: a * x = a * x9
[a,x9] in [: the carrier of L, the carrier of A:] by ZFMISC_1:87;
hence a * x = ( the lmult of B | [: the carrier of L, the carrier of A:]) . [a,x9] by A1, FUNCT_1:49
.= a * x9 by Def3 ;
::_thesis: verum
end;
theorem :: POLYALG1:18
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subalgebra of B ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subalgebra of B ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
let A be non empty Subalgebra of B; ::_thesis: ex C being Subset of B st
( the carrier of A = C & C is opers_closed )
take C = the carrier of A; ::_thesis: ( C is Subset of B & the carrier of A = C & C is opers_closed )
A1: ( 1. B = 1. A & 0. B = 0. A ) by Def3;
reconsider C = C as Subset of B by Def3;
A2: for a being Element of L
for v being Element of B st v in C holds
a * v in C
proof
let a be Element of L; ::_thesis: for v being Element of B st v in C holds
a * v in C
let v be Element of B; ::_thesis: ( v in C implies a * v in C )
assume v in C ; ::_thesis: a * v in C
then reconsider x = v as Element of A ;
a * v = a * x by Th17;
hence a * v in C ; ::_thesis: verum
end;
A3: for x, y being Element of B st x in C & y in C holds
x * y in C
proof
let x, y be Element of B; ::_thesis: ( x in C & y in C implies x * y in C )
assume A4: ( x in C & y in C ) ; ::_thesis: x * y in C
reconsider x9 = x, y9 = y as Element of B ;
reconsider x1 = x9, y1 = y9 as Element of A by A4;
x * y = x1 * y1 by Th16;
hence x * y in C ; ::_thesis: verum
end;
for v, u being Element of B st v in C & u in C holds
v + u in C
proof
let v, u be Element of B; ::_thesis: ( v in C & u in C implies v + u in C )
assume ( v in C & u in C ) ; ::_thesis: v + u in C
then reconsider x = u, y = v as Element of A ;
v + u = y + x by Th15;
hence v + u in C ; ::_thesis: verum
end;
then C is linearly-closed by A2, VECTSP_4:def_1;
hence ( C is Subset of B & the carrier of A = C & C is opers_closed ) by A1, A3, Def4; ::_thesis: verum
end;
theorem Th19: :: POLYALG1:19
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being Subset of B st A is opers_closed holds
ex C being strict Subalgebra of B st the carrier of C = A
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being Subset of B st A is opers_closed holds
ex C being strict Subalgebra of B st the carrier of C = A
let B be non empty AlgebraStr over L; ::_thesis: for A being Subset of B st A is opers_closed holds
ex C being strict Subalgebra of B st the carrier of C = A
let A be Subset of B; ::_thesis: ( A is opers_closed implies ex C being strict Subalgebra of B st the carrier of C = A )
assume A1: A is opers_closed ; ::_thesis: ex C being strict Subalgebra of B st the carrier of C = A
reconsider z = 0. B as Element of A by A1, Def4;
reconsider f4 = the lmult of B | [: the carrier of L,A:] as Function ;
A2: for x being set st x in [: the carrier of L,A:] holds
f4 . x in A
proof
A3: A is linearly-closed by A1, Def4;
let x be set ; ::_thesis: ( x in [: the carrier of L,A:] implies f4 . x in A )
assume A4: x in [: the carrier of L,A:] ; ::_thesis: f4 . x in A
consider y, z being set such that
A5: y in the carrier of L and
A6: z in A and
A7: x = [y,z] by A4, ZFMISC_1:def_2;
reconsider z = z as Element of B by A6;
reconsider y = y as Element of L by A5;
f4 . x = y * z by A4, A7, FUNCT_1:49;
hence f4 . x in A by A6, A3, VECTSP_4:def_1; ::_thesis: verum
end;
[: the carrier of L,A:] c= [: the carrier of L, the carrier of B:] by ZFMISC_1:96;
then [: the carrier of L,A:] c= dom the lmult of B by Th2;
then dom f4 = [: the carrier of L,A:] by RELAT_1:62;
then reconsider lm = f4 as Function of [: the carrier of L,A:],A by A2, FUNCT_2:3;
reconsider f1 = the addF of B || A as Function ;
reconsider f2 = the multF of B || A as Function ;
A8: for x being set st x in [:A,A:] holds
f2 . x in A
proof
let x be set ; ::_thesis: ( x in [:A,A:] implies f2 . x in A )
assume A9: x in [:A,A:] ; ::_thesis: f2 . x in A
consider y, z being set such that
A10: ( y in A & z in A ) and
A11: x = [y,z] by A9, ZFMISC_1:def_2;
reconsider y = y, z = z as Element of B by A10;
f2 . x = y * z by A9, A11, FUNCT_1:49;
hence f2 . x in A by A1, A10, Def4; ::_thesis: verum
end;
A12: [:A,A:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;
then [:A,A:] c= dom the multF of B by Th1;
then dom f2 = [:A,A:] by RELAT_1:62;
then reconsider mu = f2 as BinOp of A by A8, FUNCT_2:3;
( dom f1 = [:A,A:] & ( for x being set st x in [:A,A:] holds
f1 . x in A ) )
proof
[:A,A:] c= dom the addF of B by A12, Th1;
hence dom f1 = [:A,A:] by RELAT_1:62; ::_thesis: for x being set st x in [:A,A:] holds
f1 . x in A
let x be set ; ::_thesis: ( x in [:A,A:] implies f1 . x in A )
assume A13: x in [:A,A:] ; ::_thesis: f1 . x in A
consider y, z being set such that
A14: ( y in A & z in A ) and
A15: x = [y,z] by A13, ZFMISC_1:def_2;
A16: A is linearly-closed by A1, Def4;
reconsider y = y, z = z as Element of B by A14;
f1 . x = y + z by A13, A15, FUNCT_1:49;
hence f1 . x in A by A14, A16, VECTSP_4:def_1; ::_thesis: verum
end;
then reconsider ad = f1 as BinOp of A by FUNCT_2:3;
reconsider u = 1. B as Element of A by A1, Def4;
set c = AlgebraStr(# A,ad,mu,z,u,lm #);
( 1. AlgebraStr(# A,ad,mu,z,u,lm #) = 1. B & 0. AlgebraStr(# A,ad,mu,z,u,lm #) = 0. B ) ;
then reconsider C = AlgebraStr(# A,ad,mu,z,u,lm #) as strict Subalgebra of B by Def3;
take C ; ::_thesis: the carrier of C = A
thus the carrier of C = A ; ::_thesis: verum
end;
theorem Th20: :: POLYALG1:20
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subset of B
for X being Subset-Family of B st ( for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ) holds
meet X is opers_closed
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subset of B
for X being Subset-Family of B st ( for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ) holds
meet X is opers_closed
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subset of B
for X being Subset-Family of B st ( for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ) holds
meet X is opers_closed
let A be non empty Subset of B; ::_thesis: for X being Subset-Family of B st ( for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ) holds
meet X is opers_closed
let X be Subset-Family of B; ::_thesis: ( ( for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ) implies meet X is opers_closed )
assume A1: for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) ; ::_thesis: meet X is opers_closed
B is Subalgebra of B by Th11;
then A2: X <> {} by A1;
A3: for x, y being Element of B st x in meet X & y in meet X holds
x + y in meet X
proof
let x, y be Element of B; ::_thesis: ( x in meet X & y in meet X implies x + y in meet X )
assume A4: ( x in meet X & y in meet X ) ; ::_thesis: x + y in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
x_+_y_in_Y
reconsider x9 = x, y9 = y as Element of B ;
let Y be set ; ::_thesis: ( Y in X implies x + y in Y )
assume A5: Y in X ; ::_thesis: x + y in Y
then consider C being Subalgebra of B such that
A6: Y = the carrier of C and
A7: A c= Y by A1;
reconsider C = C as non empty Subalgebra of B by A6, A7;
reconsider x1 = x9, y1 = y9 as Element of C by A4, A5, A6, SETFAM_1:def_1;
x + y = x1 + y1 by Th15;
hence x + y in Y by A6; ::_thesis: verum
end;
hence x + y in meet X by A2, SETFAM_1:def_1; ::_thesis: verum
end;
for a being Element of L
for v being Element of B st v in meet X holds
a * v in meet X
proof
let a be Element of L; ::_thesis: for v being Element of B st v in meet X holds
a * v in meet X
let v be Element of B; ::_thesis: ( v in meet X implies a * v in meet X )
assume A8: v in meet X ; ::_thesis: a * v in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
a_*_v_in_Y
let Y be set ; ::_thesis: ( Y in X implies a * v in Y )
assume A9: Y in X ; ::_thesis: a * v in Y
then consider C being Subalgebra of B such that
A10: Y = the carrier of C and
A11: A c= Y by A1;
reconsider C = C as non empty Subalgebra of B by A10, A11;
reconsider v9 = v as Element of C by A8, A9, A10, SETFAM_1:def_1;
a * v = a * v9 by Th17;
hence a * v in Y by A10; ::_thesis: verum
end;
hence a * v in meet X by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet X is linearly-closed by A3, VECTSP_4:def_1; :: according to POLYALG1:def_4 ::_thesis: ( ( for x, y being Element of B st x in meet X & y in meet X holds
x * y in meet X ) & 1. B in meet X & 0. B in meet X )
thus for x, y being Element of B st x in meet X & y in meet X holds
x * y in meet X ::_thesis: ( 1. B in meet X & 0. B in meet X )
proof
let x, y be Element of B; ::_thesis: ( x in meet X & y in meet X implies x * y in meet X )
assume A12: ( x in meet X & y in meet X ) ; ::_thesis: x * y in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
x_*_y_in_Y
reconsider x9 = x, y9 = y as Element of B ;
let Y be set ; ::_thesis: ( Y in X implies x * y in Y )
assume A13: Y in X ; ::_thesis: x * y in Y
then consider C being Subalgebra of B such that
A14: Y = the carrier of C and
A15: A c= Y by A1;
reconsider C = C as non empty Subalgebra of B by A14, A15;
reconsider x1 = x9, y1 = y9 as Element of C by A12, A13, A14, SETFAM_1:def_1;
x * y = x1 * y1 by Th16;
hence x * y in Y by A14; ::_thesis: verum
end;
hence x * y in meet X by A2, SETFAM_1:def_1; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
1._B_in_Y
let Y be set ; ::_thesis: ( Y in X implies 1. B in Y )
assume Y in X ; ::_thesis: 1. B in Y
then consider C being Subalgebra of B such that
A16: Y = the carrier of C and
A17: A c= Y by A1;
reconsider C = C as non empty Subalgebra of B by A16, A17;
1. B = 1. C by Def3;
hence 1. B in Y by A16; ::_thesis: verum
end;
hence 1. B in meet X by A2, SETFAM_1:def_1; ::_thesis: 0. B in meet X
now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
0._B_in_Y
let Y be set ; ::_thesis: ( Y in X implies 0. B in Y )
assume Y in X ; ::_thesis: 0. B in Y
then consider C being Subalgebra of B such that
A18: Y = the carrier of C and
A19: A c= Y by A1;
reconsider C = C as non empty Subalgebra of B by A18, A19;
0. B = 0. C by Def3;
hence 0. B in Y by A18; ::_thesis: verum
end;
hence 0. B in meet X by A2, SETFAM_1:def_1; ::_thesis: verum
end;
definition
let L be non empty multMagma ;
let B be non empty AlgebraStr over L;
let A be non empty Subset of B;
func GenAlg A -> non empty strict Subalgebra of B means :Def5: :: POLYALG1:def 5
( A c= the carrier of it & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of it c= the carrier of C ) );
existence
ex b1 being non empty strict Subalgebra of B st
( A c= the carrier of b1 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b1 c= the carrier of C ) )
proof
defpred S1[ set ] means ex C being Subalgebra of B st
( $1 = the carrier of C & A c= $1 );
consider X being Subset-Family of B such that
A1: for Y being Subset of B holds
( Y in X iff S1[Y] ) from SUBSET_1:sch_3();
A2: now__::_thesis:_for_Y_being_set_st_Y_in_X_holds_
A_c=_Y
let Y be set ; ::_thesis: ( Y in X implies A c= Y )
assume Y in X ; ::_thesis: A c= Y
then ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) by A1;
hence A c= Y ; ::_thesis: verum
end;
set M = meet X;
for Y being set holds
( Y in X iff ( Y c= the carrier of B & ex C being Subalgebra of B st
( Y = the carrier of C & A c= Y ) ) ) by A1;
then A3: meet X is opers_closed by Th20;
then consider C being strict Subalgebra of B such that
A4: meet X = the carrier of C by Th19;
reconsider C = C as non empty strict Subalgebra of B by A3, A4, Def4;
take C ; ::_thesis: ( A c= the carrier of C & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of C c= the carrier of C ) )
( B is Subalgebra of B & the carrier of B in bool the carrier of B ) by Th11, ZFMISC_1:def_1;
then X <> {} by A1;
hence A c= the carrier of C by A4, A2, SETFAM_1:5; ::_thesis: for C being Subalgebra of B st A c= the carrier of C holds
the carrier of C c= the carrier of C
let C1 be Subalgebra of B; ::_thesis: ( A c= the carrier of C1 implies the carrier of C c= the carrier of C1 )
assume A5: A c= the carrier of C1 ; ::_thesis: the carrier of C c= the carrier of C1
the carrier of C1 c= the carrier of B by Def3;
then the carrier of C1 in X by A1, A5;
hence the carrier of C c= the carrier of C1 by A4, SETFAM_1:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict Subalgebra of B st A c= the carrier of b1 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b1 c= the carrier of C ) & A c= the carrier of b2 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b2 c= the carrier of C ) holds
b1 = b2
proof
let P1, P2 be non empty strict Subalgebra of B; ::_thesis: ( A c= the carrier of P1 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of P2 c= the carrier of C ) implies P1 = P2 )
assume ( A c= the carrier of P1 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of P1 c= the carrier of C ) & A c= the carrier of P2 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of P2 c= the carrier of C ) ) ; ::_thesis: P1 = P2
then A6: ( the carrier of P1 c= the carrier of P2 & the carrier of P2 c= the carrier of P1 ) ;
then A7: the carrier of P1 = the carrier of P2 by XBOOLE_0:def_10;
now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_multF_of_P1_._(x,y)_=_the_multF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the multF of P1 . (x,y) = the multF of P2 . (x,y)
let y be Element of P2; ::_thesis: the multF of P1 . (x,y) = the multF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A6, XBOOLE_0:def_10;
reconsider x1 = x as Element of P2 by A6, XBOOLE_0:def_10;
A8: the carrier of P2 c= the carrier of B by Def3;
then reconsider x9 = x1 as Element of B by TARSKI:def_3;
reconsider y9 = y as Element of B by A8, TARSKI:def_3;
thus the multF of P1 . (x,y) = x * y1
.= x9 * y9 by Th16
.= x1 * y by Th16
.= the multF of P2 . (x,y) ; ::_thesis: verum
end;
then A9: the multF of P1 = the multF of P2 by A7, BINOP_1:2;
A10: 0. P1 = 0. B by Def3
.= 0. P2 by Def3 ;
A11: now__::_thesis:_for_x_being_Element_of_L
for_y_being_Element_of_P1_holds_the_lmult_of_P1_._(x,y)_=_the_lmult_of_P2_._(x,y)
let x be Element of L; ::_thesis: for y being Element of P1 holds the lmult of P1 . (x,y) = the lmult of P2 . (x,y)
let y be Element of P1; ::_thesis: the lmult of P1 . (x,y) = the lmult of P2 . (x,y)
reconsider y1 = y as Element of P2 by A6, XBOOLE_0:def_10;
the carrier of P2 c= the carrier of B by Def3;
then reconsider y9 = y1 as Element of B by TARSKI:def_3;
thus the lmult of P1 . (x,y) = x * y
.= x * y9 by Th17
.= x * y1 by Th17
.= the lmult of P2 . (x,y) ; ::_thesis: verum
end;
A12: 1. P1 = 1. B by Def3
.= 1. P2 by Def3 ;
now__::_thesis:_for_x_being_Element_of_P1
for_y_being_Element_of_P2_holds_the_addF_of_P1_._(x,y)_=_the_addF_of_P2_._(x,y)
let x be Element of P1; ::_thesis: for y being Element of P2 holds the addF of P1 . (x,y) = the addF of P2 . (x,y)
let y be Element of P2; ::_thesis: the addF of P1 . (x,y) = the addF of P2 . (x,y)
reconsider y1 = y as Element of P1 by A6, XBOOLE_0:def_10;
reconsider x1 = x as Element of P2 by A6, XBOOLE_0:def_10;
A13: the carrier of P2 c= the carrier of B by Def3;
then reconsider x9 = x1 as Element of B by TARSKI:def_3;
reconsider y9 = y as Element of B by A13, TARSKI:def_3;
thus the addF of P1 . (x,y) = x + y1
.= x9 + y9 by Th15
.= x1 + y by Th15
.= the addF of P2 . (x,y) ; ::_thesis: verum
end;
then the addF of P1 = the addF of P2 by A7, BINOP_1:2;
hence P1 = P2 by A7, A9, A10, A12, A11, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines GenAlg POLYALG1:def_5_:_
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subset of B
for b4 being non empty strict Subalgebra of B holds
( b4 = GenAlg A iff ( A c= the carrier of b4 & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b4 c= the carrier of C ) ) );
theorem Th21: :: POLYALG1:21
for L being non empty multMagma
for B being non empty AlgebraStr over L
for A being non empty Subset of B st A is opers_closed holds
the carrier of (GenAlg A) = A
proof
let L be non empty multMagma ; ::_thesis: for B being non empty AlgebraStr over L
for A being non empty Subset of B st A is opers_closed holds
the carrier of (GenAlg A) = A
let B be non empty AlgebraStr over L; ::_thesis: for A being non empty Subset of B st A is opers_closed holds
the carrier of (GenAlg A) = A
let A be non empty Subset of B; ::_thesis: ( A is opers_closed implies the carrier of (GenAlg A) = A )
assume A is opers_closed ; ::_thesis: the carrier of (GenAlg A) = A
then ex C being strict Subalgebra of B st the carrier of C = A by Th19;
then A1: the carrier of (GenAlg A) c= A by Def5;
A c= the carrier of (GenAlg A) by Def5;
hence the carrier of (GenAlg A) = A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
func Polynom-Algebra L -> non empty strict AlgebraStr over L means :Def6: :: POLYALG1:def 6
ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & it = GenAlg A );
existence
ex b1 being non empty strict AlgebraStr over L ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b1 = GenAlg A )
proof
the carrier of (Polynom-Ring L) c= the carrier of (Formal-Series L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (Polynom-Ring L) or x in the carrier of (Formal-Series L) )
assume x in the carrier of (Polynom-Ring L) ; ::_thesis: x in the carrier of (Formal-Series L)
then x is AlgSequence of L by POLYNOM3:def_10;
hence x in the carrier of (Formal-Series L) by Def2; ::_thesis: verum
end;
then reconsider A = the carrier of (Polynom-Ring L) as non empty Subset of (Formal-Series L) ;
take GenAlg A ; ::_thesis: ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & GenAlg A = GenAlg A )
thus ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & GenAlg A = GenAlg A ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict AlgebraStr over L st ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b1 = GenAlg A ) & ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b2 = GenAlg A ) holds
b1 = b2 ;
end;
:: deftheorem Def6 defines Polynom-Algebra POLYALG1:def_6_:_
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b2 being non empty strict AlgebraStr over L holds
( b2 = Polynom-Algebra L iff ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b2 = GenAlg A ) );
registration
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
cluster Polynom-Ring L -> Loop-like ;
coherence
Polynom-Ring L is Loop-like
proof
A1: for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st x + a = b
proof
let a, b be Element of (Polynom-Ring L); ::_thesis: ex x being Element of (Polynom-Ring L) st x + a = b
reconsider x = b - a as Element of (Polynom-Ring L) ;
take x ; ::_thesis: x + a = b
thus x + a = b + ((- a) + a) by RLVECT_1:def_3
.= b + (0. (Polynom-Ring L)) by RLVECT_1:5
.= b by RLVECT_1:4 ; ::_thesis: verum
end;
A2: for a, x, y being Element of (Polynom-Ring L) st x + a = y + a holds
x = y by RLVECT_1:8;
( ( for a, b being Element of (Polynom-Ring L) ex x being Element of (Polynom-Ring L) st a + x = b ) & ( for a, x, y being Element of (Polynom-Ring L) st a + x = a + y holds
x = y ) ) by RLVECT_1:7, RLVECT_1:8;
hence Polynom-Ring L is Loop-like by A1, A2, ALGSTR_1:6; ::_thesis: verum
end;
end;
theorem Th22: :: POLYALG1:22
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds
A is opers_closed
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds
A is opers_closed
set B = Formal-Series L;
let A be non empty Subset of (Formal-Series L); ::_thesis: ( A = the carrier of (Polynom-Ring L) implies A is opers_closed )
assume A1: A = the carrier of (Polynom-Ring L) ; ::_thesis: A is opers_closed
A2: for a being Element of L
for v being Element of (Formal-Series L) st v in A holds
a * v in A
proof
let a be Element of L; ::_thesis: for v being Element of (Formal-Series L) st v in A holds
a * v in A
let v be Element of (Formal-Series L); ::_thesis: ( v in A implies a * v in A )
assume v in A ; ::_thesis: a * v in A
then reconsider p = v as AlgSequence of L by A1, POLYNOM3:def_10;
reconsider a9 = a as Element of L ;
a * v = a9 * p by Def2;
hence a * v in A by A1, POLYNOM3:def_10; ::_thesis: verum
end;
for v, u being Element of (Formal-Series L) st v in A & u in A holds
v + u in A
proof
let v, u be Element of (Formal-Series L); ::_thesis: ( v in A & u in A implies v + u in A )
assume ( v in A & u in A ) ; ::_thesis: v + u in A
then reconsider p = v, q = u as AlgSequence of L by A1, POLYNOM3:def_10;
v + u = p + q by Def2;
hence v + u in A by A1, POLYNOM3:def_10; ::_thesis: verum
end;
hence A is linearly-closed by A2, VECTSP_4:def_1; :: according to POLYALG1:def_4 ::_thesis: ( ( for x, y being Element of (Formal-Series L) st x in A & y in A holds
x * y in A ) & 1. (Formal-Series L) in A & 0. (Formal-Series L) in A )
thus for u, v being Element of (Formal-Series L) st u in A & v in A holds
u * v in A ::_thesis: ( 1. (Formal-Series L) in A & 0. (Formal-Series L) in A )
proof
let u, v be Element of (Formal-Series L); ::_thesis: ( u in A & v in A implies u * v in A )
assume ( u in A & v in A ) ; ::_thesis: u * v in A
then reconsider p = u, q = v as AlgSequence of L by A1, POLYNOM3:def_10;
u * v = p *' q by Def2;
hence u * v in A by A1, POLYNOM3:def_10; ::_thesis: verum
end;
1. (Formal-Series L) = 1_. L by Def2
.= 1. (Polynom-Ring L) by POLYNOM3:def_10 ;
hence 1. (Formal-Series L) in A by A1; ::_thesis: 0. (Formal-Series L) in A
0. (Formal-Series L) = 0_. L by Def2
.= 0. (Polynom-Ring L) by POLYNOM3:def_10 ;
hence 0. (Formal-Series L) in A by A1; ::_thesis: verum
end;
theorem :: POLYALG1:23
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr holds doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L
proof
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L
A1: ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & Polynom-Algebra L = GenAlg A ) by Def6;
then A2: the carrier of (Polynom-Algebra L) = the carrier of (Polynom-Ring L) by Th21, Th22;
A3: the carrier of (Polynom-Algebra L) c= the carrier of (Formal-Series L) by A1, Def3;
A4: for x being Element of (Polynom-Algebra L)
for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)
proof
let x be Element of (Polynom-Algebra L); ::_thesis: for y being Element of (Polynom-Ring L) holds the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)
let y be Element of (Polynom-Ring L); ::_thesis: the addF of (Polynom-Algebra L) . (x,y) = the addF of (Polynom-Ring L) . (x,y)
reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;
reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def_3;
reconsider x9 = x as Element of (Formal-Series L) by A3, TARSKI:def_3;
reconsider p = x as AlgSequence of L by A2, POLYNOM3:def_10;
reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;
reconsider q = y as AlgSequence of L by POLYNOM3:def_10;
thus the addF of (Polynom-Algebra L) . (x,y) = x + y1
.= x9 + y9 by A1, Th15
.= p + q by Def2
.= x1 + y by POLYNOM3:def_10
.= the addF of (Polynom-Ring L) . (x,y) ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_(Polynom-Algebra_L)
for_y_being_Element_of_(Polynom-Ring_L)_holds_the_multF_of_(Polynom-Algebra_L)_._(x,y)_=_the_multF_of_(Polynom-Ring_L)_._(x,y)
let x be Element of (Polynom-Algebra L); ::_thesis: for y being Element of (Polynom-Ring L) holds the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)
let y be Element of (Polynom-Ring L); ::_thesis: the multF of (Polynom-Algebra L) . (x,y) = the multF of (Polynom-Ring L) . (x,y)
reconsider y1 = y as Element of (Polynom-Algebra L) by A1, Th21, Th22;
reconsider y9 = y1 as Element of (Formal-Series L) by A1, TARSKI:def_3;
reconsider x9 = x as Element of (Formal-Series L) by A3, TARSKI:def_3;
reconsider p = x as AlgSequence of L by A2, POLYNOM3:def_10;
reconsider x1 = x as Element of (Polynom-Ring L) by A1, Th21, Th22;
reconsider q = y as AlgSequence of L by POLYNOM3:def_10;
thus the multF of (Polynom-Algebra L) . (x,y) = x * y1
.= x9 * y9 by A1, Th16
.= p *' q by Def2
.= x1 * y by POLYNOM3:def_10
.= the multF of (Polynom-Ring L) . (x,y) ; ::_thesis: verum
end;
then A5: the multF of (Polynom-Algebra L) = the multF of (Polynom-Ring L) by A2, BINOP_1:2;
A6: 1. (Polynom-Algebra L) = 1. (Formal-Series L) by A1, Def3
.= 1_. L by Def2
.= 1. (Polynom-Ring L) by POLYNOM3:def_10 ;
0. (Polynom-Algebra L) = 0. (Formal-Series L) by A1, Def3
.= 0_. L by Def2
.= 0. (Polynom-Ring L) by POLYNOM3:def_10 ;
hence doubleLoopStr(# the carrier of (Polynom-Algebra L), the addF of (Polynom-Algebra L), the multF of (Polynom-Algebra L), the OneF of (Polynom-Algebra L), the ZeroF of (Polynom-Algebra L) #) = Polynom-Ring L by A2, A4, A5, A6, BINOP_1:2; ::_thesis: verum
end;
theorem :: POLYALG1:24
for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr holds 1_ (Formal-Series L) = 1_. L by Def2;