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


definition
let F be 1-sorted ;
attr c2 is strict ;
struct AlgebraStr over F -> doubleLoopStr , ModuleStr over F;
aggr AlgebraStr(# 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 end;
end;

definition
let L be non empty doubleLoopStr ;
let A be non empty AlgebraStr over L;
attr A 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 distributive vector-distributive scalar-distributive scalar-associative scalar-unital 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 end;
end;

definition
let L be non empty doubleLoopStr ;
mode Algebra of L is non empty distributive vector-distributive scalar-distributive scalar-associative scalar-unital 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 end;

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

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

registration
let L be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
cluster Formal-Series L -> non empty commutative strict ;
coherence
Formal-Series L is commutative
proof end;
end;

registration
let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
cluster Formal-Series L -> non empty associative strict ;
coherence
Formal-Series L is associative
proof end;
end;

registration
cluster non empty right_complementable left_zeroed well-unital distributive add-associative right_zeroed associative 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 end;
end;

theorem :: POLYALG1:3
canceled;

theorem :: POLYALG1:4
canceled;

theorem :: POLYALG1:5
canceled;

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, POLYNOM3:36 ; :: 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 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 end;
cluster Formal-Series L -> non empty left-distributive strict ;
coherence
Formal-Series L is left-distributive
proof 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 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 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 end;

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

registration
let L be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative 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 end;
end;

theorem Th10: :: POLYALG1:10
for L being non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr
for a being Element of L
for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
proof end;

registration
let L be non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
cluster Formal-Series L -> non empty strict mix-associative ;
coherence
Formal-Series L is mix-associative
proof 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 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 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 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 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 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 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 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 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: :: 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 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 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 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 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 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 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 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 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 end;

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