:: 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 c₂ 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 b₁ being AlgebraStr over L st
( b₁ is strict & not b₁ 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 b₁ being non empty AlgebraStr over L st
( b₁ is unital & b₁ is distributive & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is scalar-unital & b₁ 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 b₁ being non empty strict AlgebraStr over L st
( ( for x being set holds
( x in the carrier of b₁ iff x is sequence of L ) ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
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 b₁
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b₁ = 0_. L & 1. b₁ = 1_. L )

proof end;

uniqueness
for b₁, b₂ being non empty strict AlgebraStr over L st ( for x being set holds
( x in the carrier of b₁ iff x is sequence of L ) ) & ( for x, y being Element of b₁
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₁
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 b₁
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b₁ = 0_. L & 1. b₁ = 1_. L & ( for x being set holds
( x in the carrier of b₂ iff x is sequence of L ) ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
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 b₂
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b₂ = 0_. L & 1. b₂ = 1_. L holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Formal-Series POLYALG1:def 2 :
for L being non empty doubleLoopStr
for b₂ being non empty strict AlgebraStr over L holds
( b₂ = Formal-Series L iff ( ( for x being set holds
( x in the carrier of b₂ iff x is sequence of L ) ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
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 b₂
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b₂ = 0_. L & 1. b₂ = 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 b₁ being non empty doubleLoopStr st
( b₁ is add-associative & b₁ is associative & b₁ is right_zeroed & b₁ is left_zeroed & b₁ is well-unital & b₁ is right_complementable & b₁ 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 b₁ being AlgebraStr over L st
( the carrier of b₁ c= the carrier of A & 1. b₁ = 1. A & 0. b₁ = 0. A & the addF of b₁ = the addF of A || the carrier of b₁ & the multF of b₁ = the multF of A || the carrier of b₁ & the lmult of b₁ = the lmult of A | [: the carrier of L, the carrier of b₁:] )

proof end;

end;

:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :
for L being 1-sorted
for A, b₃ being AlgebraStr over L holds
( b₃ is Subalgebra of A iff ( the carrier of b₃ c= the carrier of A & 1. b₃ = 1. A & 0. b₃ = 0. A & the addF of b₃ = the addF of A || the carrier of b₃ & the multF of b₃ = the multF of A || the carrier of b₃ & the lmult of b₃ = the lmult of A | [: the carrier of L, the carrier of b₃:] ) );

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 b₁ being AlgebraStr over L st
( not b₁ is empty & b₁ 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 b₁ being Subalgebra of B st b₁ 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 b₁ being Subalgebra of B st
( b₁ is strict & not b₁ 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 b₁ being non empty strict Subalgebra of B st
( A c= the carrier of b₁ & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b₁ c= the carrier of C ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict Subalgebra of B st A c= the carrier of b₁ & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b₁ c= the carrier of C ) & A c= the carrier of b₂ & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b₂ c= the carrier of C ) holds
b₁ = b₂

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 b₄ being non empty strict Subalgebra of B holds
( b₄ = GenAlg A iff ( A c= the carrier of b₄ & ( for C being Subalgebra of B st A c= the carrier of C holds
the carrier of b₄ 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 b₁ 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) & b₁ = GenAlg A )

proof end;

uniqueness
for b₁, b₂ 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) & b₁ = GenAlg A ) & ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b₂ = GenAlg A ) holds
b₁ = b₂ ;

end;

:: deftheorem Def6 defines Polynom-Algebra POLYALG1:def 6 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b₂ being non empty strict AlgebraStr over L holds
( b₂ = Polynom-Algebra L iff ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b₂ = 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;