:: The Algebra of Polynomials
:: by Ewa Gr\c{a}dzka
::
:: Received February 24, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


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 )
proofend;
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 )
proofend;
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:]
proofend;

theorem Th2: :: POLYALG1:2
for X, Y being set
for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
proofend;

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 )
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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
proofend;
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 )
proofend;
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)
proofend;

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))
proofend;

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

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_&amp;_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 &amp; 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 &amp; e * x = x ) )
reconsider a = x, b = e as sequence of L by Def2;
assume A1: e = 1_. L ; ::_thesis: ( x * e = x &amp; 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
proofend;
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
proofend;
cluster Formal-Series L ->  non empty left-distributive strict ;
coherence
 Formal-Series L is left-distributive
proofend;
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)
proofend;

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)
proofend;

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)
proofend;

theorem Th9: :: POLYALG1:9
for L being non empty associative well-unital doubleLoopStr
for p being sequence of L holds (1. L) * p = p
proofend;

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 &amp; Formal-Series L is scalar-distributive &amp; Formal-Series L is scalar-associative &amp; Formal-Series L is scalar-unital )
proofend;
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
proofend;

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
proofend;
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 &amp; 1. it = 1. A &amp; 0. it = 0. A &amp; the addF of it = the addF of A || the carrier of it &amp; the multF of it = the multF of A || the carrier of it &amp; 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 &amp; 1. b1 = 1. A &amp; 0. b1 = 0. A &amp; the addF of b1 = the addF of A || the carrier of b1 &amp; the multF of b1 = the multF of A || the carrier of b1 &amp; the lmult of b1 = the lmult of A | [: the carrier of L, the carrier of b1:] )
proofend;
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 &amp; 1. b3 = 1. A &amp; 0. b3 = 0. A &amp; the addF of b3 = the addF of A || the carrier of b3 &amp; the multF of b3 = the multF of A || the carrier of b3 &amp; 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
proofend;

theorem :: POLYALG1:12
for L being 1-sorted
for A, B, C being AlgebraStr over L st A is Subalgebra of B &amp; B is Subalgebra of C holds
A is Subalgebra of C
proofend;

theorem :: POLYALG1:13
for L being 1-sorted
for A, B being AlgebraStr over L st A is Subalgebra of B &amp; 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 #)
proofend;

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

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 &amp; b1 is strict )
proofend;
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
proofend;
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 &amp; not b1 is empty )
proofend;
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 &amp; ( for x, y being Element of B st x in A &amp; y in A holds
x * y in A ) &amp; 1. B in A &amp; 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 &amp; ( for x, y being Element of B st x in A &amp; y in A holds
x * y in A ) &amp; 1. B in A &amp; 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 &amp; y = y9 holds
x + y = x9 + y9
proofend;

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 &amp; y = y9 holds
x * y = x9 * y9
proofend;

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

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 &amp; C is opers_closed )
proofend;

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

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 &amp; ex C being Subalgebra of B st
( Y = the carrier of C &amp; A c= Y ) ) ) ) holds
meet X is opers_closed
proofend;

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 &amp; ( 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 &amp; ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b1 c= the carrier of C ) )
proofend;
uniqueness
 for b1, b2 being non empty strict Subalgebra of B st A c= the carrier of b1 &amp; ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b1 c= the carrier of C ) &amp; A c= the carrier of b2 &amp; ( 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
proofend;
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 &amp; ( 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
proofend;

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) &amp; 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) &amp; b1 = GenAlg A )
proofend;
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) &amp; b1 = GenAlg A ) &amp; ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) &amp; 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) &amp; 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
proofend;
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
proofend;

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

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;