:: POLYALG1 semantic presentation

definition

let F be 1-sorted ;
attr c₂ is strict;
struct AlgebraStr of F -> doubleLoopStr , VectSpStr of F;
aggr AlgebraStr(# carrier, add, mult, Zero, unity, lmult #) -> AlgebraStr of F;

end;

registration

let L be non empty doubleLoopStr ;
cluster non empty strict AlgebraStr of L;
existence

proof end;

end;

definition

let L be non empty doubleLoopStr ;
let A be non empty AlgebraStr of 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 :

registration

let L be non empty doubleLoopStr ;
cluster non empty unital distributive VectSp-like mix-associative AlgebraStr of L;
existence

proof end;

end;

definition

let L be non empty doubleLoopStr ;
mode Algebra of L is non empty unital distributive VectSp-like mix-associative AlgebraStr of 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 of 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 add-associative right_zeroed right_complementable doubleLoopStr ;
cluster Formal-Series L -> non empty add-associative right_zeroed 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 Abelian add-associative right_zeroed commutative strict ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

cluster non empty add-associative right_zeroed right_complementable associative right_unital distributive left_unital left_zeroed doubleLoopStr ;
existence

proof end;

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

proof end;

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)

proof end;

theorem Th5: :: POLYALG1:5

for L being non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p

proof end;

Lm1: now

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

end;

registration

let L be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
cluster Formal-Series L -> non empty add-associative right_zeroed right_complementable unital strict ;
coherence

proof end;

end;

Lm2: now

let L be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ; :: thesis:
set F = Formal-Series L;
reconsider e = 1_. L as Element of (Formal-Series L) by Def2;
for x being Element of (Formal-Series L) holds
( x * e = x & e * x = x ) by Lm1;
hence 1. (Formal-Series L) = 1_. L by GROUP_1:def 5; :: thesis:

end;

registration

let L be non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Formal-Series L -> non empty Abelian add-associative right_zeroed right_complementable right-distributive strict ;
coherence

proof end;

cluster Formal-Series L -> non empty Abelian add-associative right_zeroed right_complementable left-distributive strict ;
coherence

proof end;

end;

theorem Th6: :: POLYALG1:6

for L being non empty Abelian add-associative right_zeroed right_complementable distributive 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 Abelian add-associative right_zeroed right_complementable distributive 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 associative left_unital doubleLoopStr
for p being sequence of L holds (1. L) * p = p

proof end;

registration end;

theorem Th10: :: POLYALG1:10

for L being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_zeroed doubleLoopStr
for a being Element of L
for p, q being sequence of L holds a * (p *' q) = (a * p) *' q

proof end;

registration end;

Lm3: now

let L be 1-sorted ; :: thesis:
let A be AlgebraStr of L; :: thesis:
dom the add of A = [:the carrier of A,the carrier of A:] by Th2;
hence the add of A = the add of A || the carrier of A by RELAT_1:98; :: thesis:
dom the mult of A = [:the carrier of A,the carrier of A:] by Th2;
hence the mult of A = the mult of A || the carrier of A by RELAT_1:98; :: thesis:
dom the lmult of A = [:the carrier of L,the carrier of A:] by Th2;
hence the lmult of A = the lmult of A | [:the carrier of L,the carrier of A:] by RELAT_1:98; :: thesis:

end;

definition

let L be 1-sorted ;
let A be AlgebraStr of L;
mode Subalgebra of A -> AlgebraStr of L means :Def3: :: POLYALG1:def 3
( the carrier of it c= the carrier of A & 1_ it = 1_ A & 0. it = 0. A & the add of it = the add of A || the carrier of it & the mult of it = the mult 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 of L holds A is Subalgebra of A

proof end;

theorem :: POLYALG1:12

for L being 1-sorted
for A, B, C being AlgebraStr of 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 of L st A is Subalgebra of B & B is Subalgebra of A holds
AlgebraStr(# the carrier of A,the add of A,the mult of A,the Zero of A,the unity of A,the lmult of A #) = AlgebraStr(# the carrier of B,the add of B,the mult of B,the Zero of B,the unity of B,the lmult of B #)

proof end;

theorem Th14: :: POLYALG1:14

for L being 1-sorted
for A, B being AlgebraStr of L st AlgebraStr(# the carrier of A,the add of A,the mult of A,the Zero of A,the unity of A,the lmult of A #) = AlgebraStr(# the carrier of B,the add of B,the mult of B,the Zero of B,the unity of B,the lmult of B #) holds
( A is Subalgebra of B & B is Subalgebra of A )

proof end;

registration

let L be non empty 1-sorted ;
cluster non empty strict AlgebraStr of L;
existence

proof end;

end;

registration

let L be 1-sorted ;
let B be AlgebraStr of L;
cluster strict Subalgebra of B;
existence

proof end;

end;

registration

let L be non empty 1-sorted ;
let B be non empty AlgebraStr of L;
cluster non empty strict Subalgebra of B;
existence

proof end;

end;

definition

let L be non empty HGrStr ;
let B be non empty AlgebraStr of L;
let A be Subset of B;
attr A is opers_closed means :Def4: :: POLYALG1:def 4
( A is lineary-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 HGrStr
for B being non empty AlgebraStr of L
for A being non empty Subalgebra of B
for x, y being Element of B
for x', y' being Element of A st x = x' & y = y' holds
x + y = x' + y'

proof end;

theorem Th16: :: POLYALG1:16

for L being non empty HGrStr
for B being non empty AlgebraStr of L
for A being non empty Subalgebra of B
for x, y being Element of B
for x', y' being Element of A st x = x' & y = y' holds
x * y = x' * y'

proof end;

theorem Th17: :: POLYALG1:17

for L being non empty HGrStr
for B being non empty AlgebraStr of L
for A being non empty Subalgebra of B
for a being Element of L
for x being Element of B
for x' being Element of A st x = x' holds
a * x = a * x'

proof end;

theorem :: POLYALG1:18

canceled;

theorem :: POLYALG1:19

for L being non empty HGrStr
for B being non empty AlgebraStr of 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 Th20: :: POLYALG1:20

for L being non empty HGrStr
for B being non empty AlgebraStr of 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 Th21: :: POLYALG1:21

for L being non empty HGrStr
for B being non empty AlgebraStr of 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 HGrStr ;
let B be non empty AlgebraStr of 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 Th22: :: POLYALG1:22

for L being non empty HGrStr
for B being non empty AlgebraStr of 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 add-associative right_zeroed right_complementable distributive doubleLoopStr ;
func Polynom-Algebra L -> non empty strict AlgebraStr of 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

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines Polynom-Algebra POLYALG1:def 6 :

registration

let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring L -> Loop-like ;
coherence

proof end;

end;

theorem Th23: :: POLYALG1:23

for L being non empty add-associative right_zeroed right_complementable distributive 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:24

for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr holds doubleLoopStr(# the carrier of (Polynom-Algebra L),the add of (Polynom-Algebra L),the mult of (Polynom-Algebra L),the unity of (Polynom-Algebra L),the Zero of (Polynom-Algebra L) #) = Polynom-Ring L

proof end;

theorem :: POLYALG1:25

for L being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr holds 1. (Formal-Series L) = 1_. L by Lm2;