POLYALG1: The Algebra of Polynomials

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Formal-Series POLYALG1:def 2 :

registration

let L be non empty Abelian doubleLoopStr ;

cluster Formal-Series L -> non empty Abelian strict ;

coherence

proof end;

end;

registration

let L be non empty add-associative doubleLoopStr ;

cluster Formal-Series L -> non empty add-associative strict ;

coherence

proof end;

end;

registration

let L be non empty right_zeroed doubleLoopStr ;

cluster Formal-Series L -> non empty right_zeroed strict ;

coherence

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

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

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

proof end;

end;

registration

cluster non empty right_complementable left_zeroed well-unital distributive add-associative right_zeroed associative for doubleLoopStr ;

existence

proof end;

end;

theorem :: POLYALG1:3

canceled;

theorem :: POLYALG1:4

canceled;

theorem :: POLYALG1:5

canceled;

Lm1: now :: thesis:

let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
set F = Formal-Series L;
let x, e be Element of (Formal-Series L); :: thesis:
reconsider a = x, b = e as sequence of L by Def2;
assume A1: e = 1_. L ; :: thesis:
thus x * e = a *' b by Def2
.= x by A1, POLYNOM3:35 ; :: thesis:
thus e * x = b *' a by Def2
.= x by A1, POLYNOM3:36 ; :: thesis:

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

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

proof end;

cluster Formal-Series L -> non empty left-distributive strict ;

coherence

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

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

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

proof end;

end;

:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :

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

proof end;

end;

registration

let L be 1-sorted ;
let B be AlgebraStr over L;

cluster strict for Subalgebra of B;

existence

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

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines GenAlg POLYALG1:def 5 :

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 ;