:: 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;