:: The Algebra of Polynomials
:: by Ewa Gr\c{a}dzka
::
:: Received February 24, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCSDOM, BINOP_1,
SUBSET_1, FUNCT_1, ZFMISC_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1,
GROUP_1, LATTICES, MESFUNC1, NAT_1, ARYTM_3, SUPINF_2, POLYNOM3,
RLVECT_1, ARYTM_1, ALGSTR_1, FINSEQ_1, PARTFUN1, CARD_3, REALSET1,
TARSKI, UNIALG_2, RLSUB_1, SETFAM_1, POLYNOM1, ALGSEQ_1, POLYALG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS,
XCMPLX_0, REALSET1, STRUCT_0, ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCOP_1, FINSEQ_1, BINOP_1, NAT_D,
WSIERP_1, GROUP_1, RLVECT_1, VFUNCT_1,
VECTSP_1, NORMSP_1, POLYNOM1, ALGSTR_1, ALGSEQ_1, POLYNOM3, POLYNOM5,
VECTSP_4, XXREAL_0;
constructors BINOP_1, REALSET1, RFINSEQ, NAT_D, ALGSTR_1, VECTSP_4, POLYNOM3,
POLYNOM5, REAL_1, RELSET_1, FUNCOP_1, FVSUM_1, VFUNCT_1, WSIERP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, NAT_1, REALSET1,
STRUCT_0, VECTSP_1, FVSUM_1, POLYNOM3, POLYNOM5, BINOM, ORDINAL1,
VFUNCT_1, FUNCT_2, RELAT_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_0;
equalities VECTSP_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0;
expansions TARSKI, VECTSP_1;
theorems TARSKI, RLVECT_1, VECTSP_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1,
FINSEQ_3, BINOP_1, POLYNOM1, POLYNOM3, ZFMISC_1, POLYNOM5, BINOM,
RELAT_1, VECTSP_4, SETFAM_1, ALGSTR_1, XBOOLE_0, GROUP_1, NORMSP_1,
PARTFUN1;
schemes SUBSET_1, BINOP_1;
begin :: Preliminaries
definition
let F be 1-sorted;
struct (doubleLoopStr,ModuleStr over F) AlgebraStr over F
(# carrier -> set,
addF, multF -> BinOp of the carrier,
ZeroF, OneF -> Element of the carrier,
lmult -> Function of [:the carrier of F,the carrier:], the carrier #);
end;
registration
let L be non empty doubleLoopStr;
cluster strict non empty for AlgebraStr over L;
existence
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}, a, a, z, z, lm #);
thus thesis;
end;
end;
definition
let L be non empty doubleLoopStr, A be non empty AlgebraStr over L;
attr A is mix-associative means
for a being Element of L, x,y being Element of A holds a*(x*y) = (a*x)*y;
end;
registration
let L be non empty doubleLoopStr;
cluster unital distributive vector-distributive scalar-distributive
scalar-associative scalar-unital mix-associative for non empty
AlgebraStr over L;
existence
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}, a, a, z, z, lm #) as non empty AlgebraStr
over L;
take A;
A1: for x,y being Element of A holds x = y
proof
let x,y be Element of A;
x = 0 by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus A is unital
proof
take 1.A;
thus thesis by A1;
end;
thus A is distributive by A1;
thus A is vector-distributive by A1;
thus A is scalar-distributive by A1;
thus A is scalar-associative by A1;
thus A is scalar-unital by A1;
thus A is mix-associative by A1;
end;
end;
definition
let L be non empty doubleLoopStr;
mode Algebra of L is unital distributive vector-distributive
scalar-distributive scalar-associative scalar-unital mix-associative
non empty AlgebraStr over L;
end;
theorem Th1:
for X,Y being set for f being Function of [:X,Y:],X holds dom f = [:X,Y:]
proof
let X,Y be set;
let f be Function of [:X,Y:],X;
X is empty implies [:X,Y:] is empty by ZFMISC_1:90;
hence thesis by FUNCT_2:def 1;
end;
theorem Th2:
for X,Y being set for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
proof
let X,Y be set;
let f be Function of [:X,Y:],Y;
Y is empty implies [:X,Y:] is empty by ZFMISC_1:90;
hence thesis by FUNCT_2:def 1;
end;
begin :: The Algebra of Formal Power Series
definition
let L be non empty doubleLoopStr;
func Formal-Series L -> strict non empty AlgebraStr over L means
:Def2:
(for x be set holds x in the carrier of it iff x is sequence of L) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q holds
x+y = p+q) &
(for x,y be Element of it, p,q be sequence of L st x = p & y = q holds
x*y = p*'q) &
(for a be Element of L, x be Element of it, p be sequence of L st x = p
holds a*x = a*p) & 0.it = 0_.L & 1.it = 1_.L;
existence
proof
A1: 0_.(L) in the set of all x where x is sequence of L ;
then reconsider Ca = the set of all x where x is sequence of L
as non empty set;
reconsider Ze = 0_.(L) as Element of Ca by A1;
defpred P[set,set,set] means ex p,q be sequence of L st p=$1 & q=$2 & $3=p
+q;
A2: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca;
then consider p be sequence of L such that
A3: x=p;
y in Ca;
then consider q be sequence of L such that
A4: y=q;
p+q in Ca;
then reconsider u=p+q as Element of Ca;
take u,p,q;
thus thesis by A3,A4;
end;
consider Ad be Function of [:Ca,Ca:],Ca such that
A5: for x,y be Element of Ca holds P[x,y,Ad.(x,y)] from BINOP_1:sch 3(
A2);
1_.(L) in the set of all x where x is sequence of L ;
then reconsider Un = 1_.(L) as Element of Ca;
defpred P[set,set,set] means ex p,q be sequence of L st p=$1 & q=$2 & $3=p
*'q;
A6: for x,y be Element of Ca ex u be Element of Ca st P[x,y,u]
proof
let x,y be Element of Ca;
x in Ca;
then consider p be sequence of L such that
A7: x=p;
y in Ca;
then consider q be sequence of L such that
A8: y=q;
p*'q in Ca;
then reconsider u=p*'q as Element of Ca;
take u,p,q;
thus thesis by A7,A8;
end;
consider Mu be Function of [:Ca,Ca:],Ca such that
A9: for x,y be Element of Ca holds P[x,y,Mu.(x,y)] from BINOP_1:sch 3
(A6);
defpred P[Element of L,set,set] means ex p be sequence of L st p=$2 & $3=
$1*p;
A10: for a being Element of L,x be Element of Ca ex u be Element of Ca st
P[a,x,u]
proof
let a being Element of L,x be Element of Ca;
x in Ca;
then consider q be sequence of L such that
A11: x = q;
a*q in Ca;
then reconsider u = a*q as Element of Ca;
take u,q;
thus thesis by A11;
end;
consider lm being Function of [:the carrier of L,Ca:],Ca such that
A12: for a being Element of L,x be Element of Ca holds P[a,x,lm.(a,x)]
from BINOP_1:sch 3(A10);
reconsider P = AlgebraStr(# Ca, Ad, Mu, Ze, Un, lm #) as strict non empty
AlgebraStr over L;
take P;
thus for x be set holds x in the carrier of P iff x is sequence of L
proof
let x be set;
thus x in the carrier of P implies x is sequence of L
proof
assume x in the carrier of P;
then ex p be sequence of L st x=p;
hence thesis;
end;
thus thesis;
end;
thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds
x+y = p+q
proof
let x,y be Element of P;
let p,q be sequence of L;
assume
A13: x = p & y = q;
ex p1,q1 be sequence of L st p1 = x & q1 = y & Ad.(x,y) = p1+q1 by A5;
hence thesis by A13;
end;
thus for x,y be Element of P, p,q be sequence of L st x = p & y = q holds
x*y = p*'q
proof
let x,y be Element of P;
let p,q be sequence of L;
assume
A14: x = p & y = q;
ex p1,q1 be sequence of L st p1 = x & q1 = y & Mu.(x,y) = p1*'q1 by A9;
hence thesis by A14;
end;
thus for a be Element of L, x be Element of P, p be sequence of L st x = p
holds a*x = a*p
proof
let a be Element of L, x be Element of P, p be sequence of L such that
A15: x = p;
ex p1 being sequence of L st x = p1 & lm.(a,x)=a*p1 by A12;
hence thesis by A15;
end;
thus 0.P = 0_.(L);
thus thesis;
end;
uniqueness
proof
let P1,P2 be strict non empty AlgebraStr over L such that
A16: for x be set holds x in the carrier of P1 iff x is sequence of L and
A17: for x,y be Element of P1, p,q be sequence of L st x = p & y = q
holds x+y = p+q and
A18: for x,y be Element of P1, p,q be sequence of L st x = p & y = q
holds x*y = p*'q and
A19: for a be Element of L, x be Element of P1, p be 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 be set holds x in the carrier of P2 iff x is sequence of L and
A22: for x,y be Element of P2, p,q be sequence of L st x = p & y = q
holds x+y = p+q and
A23: for x,y be Element of P2, p,q be sequence of L st x = p & y = q
holds x*y = p*'q and
A24: for a be Element of L, x be Element of P2, p be sequence of L st
x = p holds a*x = a*p and
A25: 0.P2 = 0_.(L) & 1.P2 = 1_.(L);
A26: now
let x be object;
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;
end;
then
A27: the carrier of P1 = the carrier of P2 by TARSKI:2;
now
let a be Element of L, x be Element of P1;
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);
end;
then
A28: the lmult of P1=the lmult of P2 by A27,BINOP_1:2;
A29: now
let x be Element of P1, y be Element of P2;
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);
end;
now
let x be Element of P1, y be Element of P2;
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);
end;
then the addF of P1 = the addF of P2 by A27,BINOP_1:2;
hence thesis by A20,A25,A27,A29,A28,BINOP_1:2;
end;
end;
registration
let L be Abelian non empty doubleLoopStr;
cluster Formal-Series L -> Abelian;
coherence
proof
let p,q be Element of Formal-Series L;
reconsider p1=p, q1=q as sequence of L by Def2;
thus p + q = p1 + q1 by Def2
.= q + p by Def2;
end;
end;
registration
let L be add-associative non empty doubleLoopStr;
cluster Formal-Series L -> add-associative;
coherence
proof
let p,q,r be Element of Formal-Series L;
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;
end;
end;
registration
let L be right_zeroed non empty doubleLoopStr;
cluster Formal-Series L -> right_zeroed;
coherence
proof
let p be Element of Formal-Series L;
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;
end;
end;
registration
let L be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
cluster Formal-Series L -> right_complementable;
coherence
proof
let p be Element of Formal-Series L;
reconsider p1=p as sequence of L by Def2;
reconsider q = -p1 as Element of Formal-Series L by Def2;
take q;
thus p + q = p1 + -p1 by Def2
.= p1 - p1 by POLYNOM3:def 6
.= 0_.(L) by POLYNOM3:29
.= 0.(Formal-Series L) by Def2;
end;
end;
registration
let L be Abelian add-associative right_zeroed commutative non empty
doubleLoopStr;
cluster Formal-Series L -> commutative;
coherence
proof
let p,q be Element of Formal-Series L;
reconsider p1=p, q1=q as sequence of L by Def2;
thus p * q = p1 *' q1 by Def2
.= q * p by Def2;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative distributive non empty doubleLoopStr;
cluster Formal-Series L -> associative;
coherence
proof
let p,q,r be Element of Formal-Series L;
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;
end;
end;
registration
cluster add-associative associative right_zeroed left_zeroed well-unital
right_complementable distributive for non empty doubleLoopStr;
existence
proof
take F_Real;
thus thesis;
end;
end;
::$CT 3
Lm1: now
let L be add-associative right_zeroed right_complementable distributive
well-unital non empty doubleLoopStr;
set F = Formal-Series L;
let x, e be Element of F;
reconsider a=x, b=e as sequence of L by Def2;
assume
A1: e = 1_.L;
thus x * e = a*'b by Def2
.= x by A1,POLYNOM3:35;
thus e * x = b*'a by Def2
.= x by A1,POLYNOM3:36;
end;
registration
let L be right_zeroed add-associative right_complementable distributive
well-unital non empty doubleLoopStr;
cluster Formal-Series L -> well-unital;
coherence
proof
let x be Element of Formal-Series L;
set F = Formal-Series L;
1.F = 1_.L by Def2;
hence thesis by Lm1;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
cluster Formal-Series L -> right-distributive;
coherence
proof
let p,q,r be Element of Formal-Series L;
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;
end;
cluster Formal-Series L -> left-distributive;
coherence
proof
let p,q,r be Element of Formal-Series L;
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;
end;
end;
theorem Th6:
for L be Abelian add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr for a being Element
of L, p,q being sequence of L holds a*(p+q)=a*p + a*q
proof
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
let a be Element of L, p,q be sequence of L;
for i be Element of NAT holds (a*(p+q)).i = (a*p + a*q).i
proof
let i be Element of NAT;
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 4
.= (a*p).i + (a*q).i by POLYNOM5:def 4
.= (a*p + a*q).i by NORMSP_1:def 2;
hence thesis by POLYNOM5:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th7:
for L be Abelian add-associative right_zeroed
right_complementable distributive non empty doubleLoopStr for a,b being
Element of L, p being sequence of L holds (a+b)*p = a*p + b*p
proof
let L be Abelian add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
let a,b be Element of L, p be sequence of L;
for i be Element of NAT holds ((a+b)*p).i = (a*p + b*p).i
proof
let i be Element of NAT;
thus ((a+b)*p).i = (a+b)*p.i by POLYNOM5:def 4
.= a*p.i + b*p.i by VECTSP_1:def 7
.= (a*p).i + b*p.i by POLYNOM5:def 4
.= (a*p).i + (b*p).i by POLYNOM5:def 4
.= (a*p + b*p).i by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th8:
for L be associative non empty doubleLoopStr
for a,b being Element of L, p being sequence of L holds (a*b)*p = a*(b*p)
proof
let L be associative non empty doubleLoopStr;
let a,b be Element of L, p be sequence of L;
for i be Element of NAT holds ((a*b)*p).i = (a*(b*p)).i
proof
let i be Element of NAT;
thus ((a*b)*p).i = (a*b)*p.i by POLYNOM5:def 4
.= a*(b*(p.i)) by GROUP_1:def 3
.= a*(b*p).i by POLYNOM5:def 4
.= (a*(b*p)).i by POLYNOM5:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th9:
for L be associative well-unital non empty doubleLoopStr for p
being sequence of L holds 1.L*p = p
proof
let L be associative well-unital non empty doubleLoopStr;
let p be sequence of L;
for i being Element of NAT holds ((1.L)*p).i = p.i
proof
let i be Element of NAT;
thus ((1.L)*p).i = (1.L)*p.i by POLYNOM5:def 4
.= p.i;
end;
hence thesis by FUNCT_2:63;
end;
registration
let L be Abelian add-associative associative right_zeroed
right_complementable well-unital distributive non empty doubleLoopStr;
cluster Formal-Series L -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof set F = Formal-Series L;
thus F is vector-distributive
proof
let x be Element of L;
let v,w being Element of Formal-Series L;
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;
end;
thus F is scalar-distributive
proof
let x,y be Element of L;
let v being Element of Formal-Series L;
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;
end;
thus F is scalar-associative
proof
let x,y be Element of L;
let v being Element of Formal-Series L;
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;
end;
let v be Element of F;
reconsider p=v as sequence of L by Def2;
thus (1.L)*v = 1.L*p by Def2
.= v by Th9;
end;
end;
theorem Th10:
for L be Abelian left_zeroed add-associative associative
right_zeroed right_complementable distributive non empty doubleLoopStr for a
being Element of L, p,q being sequence of L holds a*(p*'q)=(a*p)*'q
proof
let L be Abelian left_zeroed add-associative associative right_zeroed
right_complementable distributive non empty doubleLoopStr;
let a being Element of L, p,q being sequence of L;
for x being Element of NAT holds (a*(p*'q)).x = ((a*p)*'q).x
proof
let i be Element of NAT;
consider f1 be FinSequence of the carrier of L such that
A1: len f1 = i+1 and
A2: (p*'q).i = Sum f1 and
A3: for k be Element of NAT st k in dom f1 holds f1.k = p.(k-'1) * q.(
i+1-'k) by POLYNOM3:def 9;
consider f2 be 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 be 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 be Nat st k in dom f2 holds f2.k = (a*f1).k
proof
let k be Nat such that
A9: k in dom f2;
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 4
.= 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;
end;
thus (a*(p*'q)).i = a*(Sum f1) by A2,POLYNOM5:def 4
.= Sum (a* f1) by BINOM:4
.= ((a*p)*'q).i by A5,A7,A8,FINSEQ_1:13;
end;
hence thesis by FUNCT_2:63;
end;
registration
let L be Abelian left_zeroed add-associative associative right_zeroed
right_complementable distributive non empty doubleLoopStr;
cluster Formal-Series L -> mix-associative;
coherence
proof
let a be Element of L, x,y be Element of Formal-Series L;
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;
end;
end;
definition
let L be 1-sorted;
let A be AlgebraStr over L;
mode Subalgebra of A -> AlgebraStr over L means :Def3:
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
proof
take A;
thus thesis;
end;
end;
theorem Th11:
for L being 1-sorted for A being AlgebraStr over L holds A is Subalgebra of A
proof
let L be 1-sorted;
let A be AlgebraStr over L;
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:];
end;
theorem
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;
let A,B,C be AlgebraStr over L such that
A1: A is Subalgebra of B and
A2: B 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;
thus 1.A = 1.B by A1,Def3
.= 1.C by A2,Def3;
thus 0.A = 0.B by A1,Def3
.= 0.C by A2,Def3;
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;
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;
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;
end;
theorem
for L being 1-sorted for A,B being AlgebraStr over L st
A is Subalgebra of B & B is Subalgebra of A holds
the AlgebraStr of A = the AlgebraStr of B
proof
let L be 1-sorted;
let A,B be AlgebraStr over L such that
A1: A is Subalgebra of B and
A2: B is Subalgebra of A;
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: 0.A = 0.B & 1.A = 1.B by A1,Def3;
A9: the multF of A = (the multF of B)||the carrier of A by A1,Def3
.= the multF of B by A5;
the addF of A = (the addF of B)||the carrier of A by A1,Def3
.= the addF of B by A5;
hence thesis by A4,A3,A9,A7,A8,XBOOLE_0:def 10;
end;
theorem Th14:
for L being 1-sorted for A,B being AlgebraStr over L st
the AlgebraStr of A = the AlgebraStr of B holds A is Subalgebra of B
proof
let L be 1-sorted;
let A,B be AlgebraStr over L such that
A1: the AlgebraStr of A = the AlgebraStr of B;
thus the carrier of A c= the carrier of B by A1;
thus 1.A = 1.B by A1;
thus 0.A = 0.B by A1;
thus the addF of A = (the addF of B)||the carrier of A by A1;
thus the multF of A = (the multF of B)||the carrier of A by A1;
thus thesis by A1;
end;
registration
let L be non empty 1-sorted;
cluster non empty strict for AlgebraStr over L;
existence
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 A;
take B = AlgebraStr(#{0}, a, a, z, z, lm #);
thus B is non empty;
thus thesis;
end;
end;
registration
let L be 1-sorted;
let B be AlgebraStr over L;
cluster strict for Subalgebra of B;
existence
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;
thus thesis;
end;
end;
registration
let L be non empty 1-sorted;
let B be non empty AlgebraStr over L;
cluster strict non empty for Subalgebra of B;
existence
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;
thus thesis;
end;
end;
definition
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be Subset of B;
attr A is opers_closed means
:Def4:
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;
theorem Th15:
for L being non empty multMagma for B being non empty AlgebraStr
over L for A being non empty Subalgebra of B holds for x,y being Element of B,
x9,y9 being Element of A st x = x9 & y = y9 holds x+y = x9+ y9
proof
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
let x,y be Element of B, x9,y9 be Element of A such that
A1: x = x9 & y = 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;
end;
theorem Th16:
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subalgebra of B holds for x,y being Element of B, x9,y9
being Element of A st x = x9 & y = y9 holds x*y = x9* y9
proof
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
let x,y be Element of B, x9,y9 be Element of A such that
A1: x = x9 & y = 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;
end;
theorem Th17:
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subalgebra of B holds for a being Element of L for x being
Element of B, x9 being Element of A st x = x9 holds a * x = a * x9
proof
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
let a be Element of L;
let x be Element of B, x9 be Element of A such that
A1: x = 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;
end;
theorem
for L be non empty multMagma for B be non empty AlgebraStr over L for
A be 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;
let B be non empty AlgebraStr over L;
let A be non empty Subalgebra of B;
take C = the carrier of A;
A1: 1.B = 1.A & 0.B = 0.A by Def3;
reconsider C as Subset of B by Def3;
A2: for a being Element of L, v being Element of B st v in C holds a * v in C
proof
let a be Element of L, v be Element of B;
assume v in C;
then reconsider x = v as Element of A;
a * v = a * x by Th17;
hence thesis;
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 such that
A4: x in C & 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 thesis;
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;
assume v in C & u in C;
then reconsider x = u, y = v as Element of A;
v + u = y + x by Th15;
hence thesis;
end;
then C is linearly-closed by A2,VECTSP_4:def 1;
hence thesis by A1,A3,Def4;
end;
theorem Th19:
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be Subset of B st A is opers_closed ex C being strict Subalgebra of B
st the carrier of C = A
proof
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be Subset of B such that
A1: A is opers_closed;
reconsider z = 0.B as Element of A by A1;
reconsider f4 = (the lmult of B)|[:the carrier of L,A:] as Function;
A2: for x being object st x in [:the carrier of L,A:] holds f4.x in A
proof
A3: A is linearly-closed by A1;
let x be object such that
A4: x in [:the carrier of L,A:];
consider y,z be object 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 as Element of B by A6;
reconsider y as Element of L by A5;
f4.x = y * z by A4,A7,FUNCT_1:49;
hence thesis by A6,A3,VECTSP_4:def 1;
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 object st x in [:A,A:] holds f2.x in A
proof
let x be object such that
A9: x in [:A,A:];
consider y,z be object such that
A10: y in A & z in A and
A11: x = [y,z] by A9,ZFMISC_1:def 2;
reconsider y,z as Element of B by A10;
f2.x = y * z by A9,A11,FUNCT_1:49;
hence thesis by A1,A10;
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 object 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;
let x be object such that
A13: x in [:A,A:];
consider y,z be object 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;
reconsider y,z as Element of B by A14;
f1.x = y + z by A13,A15,FUNCT_1:49;
hence thesis by A14,A16,VECTSP_4:def 1;
end;
then reconsider ad = f1 as BinOp of A by FUNCT_2:3;
reconsider u = 1.B as Element of A by A1;
set c = AlgebraStr(# A, ad, mu, z, u, lm #);
1.c = 1.B & 0.c = 0.B;
then reconsider C=c as strict Subalgebra of B by Def3;
take C;
thus thesis;
end;
theorem Th20:
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 be 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 being non empty multMagma;
let B being non empty AlgebraStr over L;
let A being non empty Subset of B;
let X being Subset-Family of B such that
A1: for Y be 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;
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 such that
A4: x in meet X & y in meet X;
now
reconsider x9 = x, y9 = y as Element of B;
let Y be set;
assume
A5: Y in X;
then consider C be Subalgebra of B such that
A6: Y = the carrier of C and
A7: A c= Y by A1;
reconsider 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;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
for a being Element of L, v being Element of B st v in meet X holds a *
v in meet X
proof
let a be Element of L, v be Element of B such that
A8: v in meet X;
now
let Y be set;
assume
A9: Y in X;
then consider C be Subalgebra of B such that
A10: Y = the carrier of C and
A11: A c= Y by A1;
reconsider 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;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
hence meet X is linearly-closed by A3,VECTSP_4:def 1;
thus 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 such that
A12: x in meet X & y in meet X;
now
reconsider x9 = x, y9 = y as Element of B;
let Y be set;
assume
A13: Y in X;
then consider C be Subalgebra of B such that
A14: Y = the carrier of C and
A15: A c= Y by A1;
reconsider 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;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
now
let Y be set;
assume Y in X;
then consider C be Subalgebra of B such that
A16: Y = the carrier of C and
A17: A c= Y by A1;
reconsider C as non empty Subalgebra of B by A16,A17;
1.B = 1.C by Def3;
hence 1.B in Y by A16;
end;
hence 1.B in meet X by A2,SETFAM_1:def 1;
now
let Y be set;
assume Y in X;
then consider C be Subalgebra of B such that
A18: Y = the carrier of C and
A19: A c= Y by A1;
reconsider C as non empty Subalgebra of B by A18,A19;
0.B = 0.C by Def3;
hence 0.B in Y by A18;
end;
hence thesis by A2,SETFAM_1:def 1;
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 -> strict non empty Subalgebra of B means
:Def5:
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
proof
defpred P[set] means ex C being Subalgebra of B st $1 = the carrier of C &
A c= $1;
consider X be Subset-Family of B such that
A1: for Y being Subset of B holds Y in X iff P[Y] from SUBSET_1:sch 3;
A2: now
let Y be set;
assume Y in X;
then ex C being Subalgebra of B st Y = the carrier of C & A c= Y by A1;
hence A c= Y;
end;
set M = meet X;
for Y be 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: M is opers_closed by Th20;
then consider C being strict Subalgebra of B such that
A4: M = the carrier of C by Th19;
reconsider C as non empty strict Subalgebra of B by A3,A4;
take 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;
let C1 be Subalgebra of B such that
A5: A 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 thesis by A4,SETFAM_1:3;
end;
uniqueness
proof
let P1,P2 be strict non empty Subalgebra of B;
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;
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
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A6;
reconsider x1=x as Element of P2 by A6;
A8: the carrier of P2 c= the carrier of B by Def3;
then reconsider x9 = x1 as Element of B;
reconsider y9 = y as Element of B by A8;
thus (the multF of P1).(x,y) = x * y1 .= x9 * y9 by Th16
.= x1 * y by Th16
.= (the multF of P2).(x,y);
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
let x be Element of L, y be Element of P1;
reconsider y1=y as Element of P2 by A6;
the carrier of P2 c= the carrier of B by Def3;
then reconsider y9 = y1 as Element of B;
thus (the lmult of P1).(x,y) = x * y .= x * y9 by Th17
.= x * y1 by Th17
.= (the lmult of P2).(x,y);
end;
A12: 1.P1 = 1.B by Def3
.= 1.P2 by Def3;
now
let x be Element of P1, y be Element of P2;
reconsider y1=y as Element of P1 by A6;
reconsider x1=x as Element of P2 by A6;
A13: the carrier of P2 c= the carrier of B by Def3;
then reconsider x9 = x1 as Element of B;
reconsider y9 = y as Element of B by A13;
thus (the addF of P1).(x,y) = x + y1 .= x9 + y9 by Th15
.= x1 + y by Th15
.= (the addF of P2).(x,y);
end;
then the addF of P1 = the addF of P2 by A7,BINOP_1:2;
hence thesis by A7,A9,A10,A12,A11,BINOP_1:2;
end;
end;
theorem Th21:
for L be non empty multMagma for B be non empty AlgebraStr over
L for A be non empty Subset of B st A is opers_closed holds the carrier of
GenAlg A = A
proof
let L be non empty multMagma;
let B be non empty AlgebraStr over L;
let A be non empty Subset of B;
assume A is opers_closed;
then ex C be 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 thesis by A1,XBOOLE_0:def 10;
end;
begin ::The Algebra of Polynomials
definition
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
func Polynom-Algebra L -> strict non empty AlgebraStr over L means
:Def6:
ex
A being non empty Subset of Formal-Series L st A = the carrier of Polynom-Ring
L & it = GenAlg A;
existence
proof
the carrier of Polynom-Ring L c= the carrier of Formal-Series L
proof
let x be object;
assume x in the carrier of Polynom-Ring L;
then x is AlgSequence of L by POLYNOM3:def 10;
hence thesis by Def2;
end;
then reconsider A = the carrier of Polynom-Ring L as non empty Subset of
Formal-Series L;
take GenAlg A;
thus thesis;
end;
uniqueness;
end;
registration
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
cluster Polynom-Ring L -> Loop-like;
coherence
proof
A1: for a,b be 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;
reconsider x = b - a as Element of Polynom-Ring L;
take x;
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;
end;
A2: for a,x,y be Element of Polynom-Ring L holds x+a=y+a implies x=y by
RLVECT_1:8;
( for a,b be Element of Polynom-Ring L ex x being Element of
Polynom-Ring L st a+x=b)& for a,x,y be Element of Polynom-Ring L holds a+x=a +y
implies x=y by RLVECT_1:7,8;
hence thesis by A1,A2,ALGSTR_1:6;
end;
end;
theorem Th22:
for L being add-associative right_zeroed right_complementable
distributive non empty 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 add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
set B = Formal-Series L;
let A be non empty Subset of Formal-Series L such that
A1: A = the carrier of Polynom-Ring L;
A2: for a being Element of L, v being Element of B st v in A holds a * v in A
proof
let a be Element of L, v being Element of B;
assume 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 thesis by A1,POLYNOM3:def 10;
end;
for v,u being Element of B st v in A & u in A holds v + u in A
proof
let v,u be Element of B;
assume v in A & 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 thesis by A1,POLYNOM3:def 10;
end;
hence A is linearly-closed by A2,VECTSP_4:def 1;
thus for u,v being Element of B st u in A & v in A holds u*v in A
proof
let u,v be Element of B;
assume u in A & 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 thesis by A1,POLYNOM3:def 10;
end;
1.B = 1_.(L) by Def2
.= 1.Polynom-Ring L by POLYNOM3:def 10;
hence 1.B in A by A1;
0.B = 0_.(L) by Def2
.= 0.(Polynom-Ring L) by POLYNOM3:def 10;
hence thesis by A1;
end;
theorem
for L be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr holds the doubleLoopStr of
Polynom-Algebra L = Polynom-Ring L
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
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, y be Element of Polynom-Ring L;
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;
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);
end;
now
let x be Element of Polynom-Algebra L, y be Element of Polynom-Ring L;
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;
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);
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 thesis by A2,A4,A5,A6,BINOP_1:2;
end;
theorem
for L being add-associative right_zeroed right_complementable
well-unital distributive non empty doubleLoopStr holds 1_Formal-Series L =
1_.L by Def2;