:: POLYALG1 semantic presentation

definition

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

end;

registration

let c₁ be non empty doubleLoopStr ;
cluster non empty strict AlgebraStr of a₁;
existence

proof end;

end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂ be non empty AlgebraStr of c₁;
attr a₂ is mix-associative means :: POLYALG1:def 1
for b₁ being Element of a₁
for b₂, b₃ being Element of a₂ holds b₁ * (b₂ * b₃) = (b₁ * b₂) * b₃;

end;

:: deftheorem Def1 defines mix-associative POLYALG1:def 1 :

registration

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

proof end;

end;

definition

let c₁ be non empty doubleLoopStr ;
mode Algebra of a₁ is non empty unital distributive VectSp-like mix-associative AlgebraStr of a₁;

end;

theorem Th1: :: POLYALG1:1

for b₁, b₂ being set
for b₃ being Function of [:b₁,b₂:],b₁ holds dom b₃ = [:b₁,b₂:]

proof end;

theorem Th2: :: POLYALG1:2

for b₁, b₂ being set
for b₃ being Function of [:b₁,b₂:],b₂ holds dom b₃ = [:b₁,b₂:]

proof end;

definition

let c₁ be non empty doubleLoopStr ;
func Formal-Series c₁ -> non empty strict AlgebraStr of a₁ means :Def2: :: POLYALG1:def 2
( ( for b₁ being set holds
( b₁ in the carrier of a₂ iff b₁ is sequence of a₁ ) ) & ( for b₁, b₂ being Element of a₂
for b₃, b₄ being sequence of a₁ st b₁ = b₃ & b₂ = b₄ holds
b₁ + b₂ = b₃ + b₄ ) & ( for b₁, b₂ being Element of a₂
for b₃, b₄ being sequence of a₁ st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ *' b₄ ) & ( for b₁ being Element of a₁
for b₂ being Element of a₂
for b₃ being sequence of a₁ st b₂ = b₃ holds
b₁ * b₂ = b₁ * b₃ ) & 0. a₂ = 0_. a₁ & 1_ a₂ = 1_. a₁ );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let c₁ be non empty Abelian doubleLoopStr ;
cluster Formal-Series a₁ -> non empty Abelian strict ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative doubleLoopStr ;
cluster Formal-Series a₁ -> non empty add-associative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed doubleLoopStr ;
cluster Formal-Series a₁ -> non empty right_zeroed strict ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
cluster Formal-Series a₁ -> non empty add-associative right_zeroed right_complementable strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
cluster Formal-Series a₁ -> non empty Abelian add-associative right_zeroed commutative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr ;
cluster Formal-Series a₁ -> 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 b₁ being non empty set
for b₂ being non empty FinSequence of b₁ holds b₂ /^ 1 = Del b₂,1

proof end;

theorem Th4: :: POLYALG1:4

for b₁ being non empty set
for b₂ being non empty FinSequence of b₁ holds b₂ = <*(b₂ . 1)*> ^ (Del b₂,1)

proof end;

theorem Th5: :: POLYALG1:5

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

proof end;

E7: now

let c₁ be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
set c₂ = Formal-Series c₁;
let c₃, c₄ be Element of (Formal-Series c₁);
assume E8: c₄ = 1_. c₁ ;
reconsider c₅ = c₃, c₆ = c₄ as sequence of c₁ by Def2;
thus c₃ * c₄ = c₅ *' c₆ by Def2
.= c₃ by E8, POLYNOM3:36 ;
thus c₄ * c₃ = c₆ *' c₅ by Def2
.= c₃ by E8, Th5 ;

end;

registration

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

proof end;

end;

E8: now

let c₁ be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
set c₂ = Formal-Series c₁;
reconsider c₃ = 1_. c₁ as Element of (Formal-Series c₁) by Def2;
for b₁ being Element of (Formal-Series c₁) holds
( b₁ * c₃ = b₁ & c₃ * b₁ = b₁ ) by Lemma7;
hence 1. (Formal-Series c₁) = 1_. c₁ by GROUP_1:def 5;

end;

registration

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

proof end;

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

proof end;

end;

theorem Th6: :: POLYALG1:6

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being Element of b₁
for b₃, b₄ being sequence of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄)

proof end;

theorem Th7: :: POLYALG1:7

for b₁ being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being sequence of b₁ holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄)

proof end;

theorem Th8: :: POLYALG1:8

for b₁ being non empty associative doubleLoopStr
for b₂, b₃ being Element of b₁
for b₄ being sequence of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

theorem Th9: :: POLYALG1:9

for b₁ being non empty associative left_unital doubleLoopStr
for b₂ being sequence of b₁ holds (1. b₁) * b₂ = b₂

proof end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
cluster Formal-Series a₁ -> non empty Abelian add-associative right_zeroed right_complementable right-distributive left-distributive VectSp-like strict ;
coherence

proof end;

end;

theorem Th10: :: POLYALG1:10

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_zeroed doubleLoopStr
for b₂ being Element of b₁
for b₃, b₄ being sequence of b₁ holds b₂ * (b₃ *' b₄) = (b₂ * b₃) *' b₄

proof end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_zeroed doubleLoopStr ;
cluster Formal-Series a₁ -> non empty Abelian add-associative right_zeroed right_complementable right-distributive left-distributive strict mix-associative ;
coherence

proof end;

end;

E14: now

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

end;

definition

let c₁ be 1-sorted ;
let c₂ be AlgebraStr of c₁;
mode Subalgebra of c₂ -> AlgebraStr of a₁ means :Def3: :: POLYALG1:def 3
( the carrier of a₃ c= the carrier of a₂ & 1_ a₃ = 1_ a₂ & 0. a₃ = 0. a₂ & the add of a₃ = the add of a₂ || the carrier of a₃ & the mult of a₃ = the mult of a₂ || the carrier of a₃ & the lmult of a₃ = the lmult of a₂ | [:the carrier of a₁,the carrier of a₃:] );
existence

proof end;

end;

:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :

theorem Th11: :: POLYALG1:11

for b₁ being 1-sorted
for b₂ being AlgebraStr of b₁ holds b₂ is Subalgebra of b₂

proof end;

theorem Th12: :: POLYALG1:12

for b₁ being 1-sorted
for b₂, b₃, b₄ being AlgebraStr of b₁ st b₂ is Subalgebra of b₃ & b₃ is Subalgebra of b₄ holds
b₂ is Subalgebra of b₄

proof end;

theorem Th13: :: POLYALG1:13

for b₁ being 1-sorted
for b₂, b₃ being AlgebraStr of b₁ st b₂ is Subalgebra of b₃ & b₃ is Subalgebra of b₂ holds
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₂ #) = 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 b₁ being 1-sorted
for b₂, b₃ being AlgebraStr of b₁ st 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₂ #) = 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
( b₂ is Subalgebra of b₃ & b₃ is Subalgebra of b₂ )

proof end;

registration

let c₁ be non empty 1-sorted ;
cluster non empty strict AlgebraStr of a₁;
existence

proof end;

end;

registration

let c₁ be 1-sorted ;
let c₂ be AlgebraStr of c₁;
cluster strict Subalgebra of a₂;
existence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty AlgebraStr of c₁;
cluster non empty strict Subalgebra of a₂;
existence

proof end;

end;

definition

let c₁ be non empty HGrStr ;
let c₂ be non empty AlgebraStr of c₁;
let c₃ be Subset of c₂;
attr a₃ is opers_closed means :Def4: :: POLYALG1:def 4
( a₃ is lineary-closed & ( for b₁, b₂ being Element of a₂ st b₁ in a₃ & b₂ in a₃ holds
b₁ * b₂ in a₃ ) & 1_ a₂ in a₃ & 0. a₂ in a₃ );

end;

:: deftheorem Def4 defines opers_closed POLYALG1:def 4 :

theorem Th15: :: POLYALG1:15

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being non empty Subalgebra of b₂
for b₄, b₅ being Element of b₂
for b₆, b₇ being Element of b₃ st b₄ = b₆ & b₅ = b₇ holds
b₄ + b₅ = b₆ + b₇

proof end;

theorem Th16: :: POLYALG1:16

proof end;

theorem Th17: :: POLYALG1:17

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being non empty Subalgebra of b₂
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Element of b₃ st b₅ = b₆ holds
b₄ * b₅ = b₄ * b₆

proof end;

theorem Th18: :: POLYALG1:18

canceled;

theorem Th19: :: POLYALG1:19

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being non empty Subalgebra of b₂ ex b₄ being Subset of b₂ st
( the carrier of b₃ = b₄ & b₄ is opers_closed )

proof end;

theorem Th20: :: POLYALG1:20

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being Subset of b₂ st b₃ is opers_closed holds
ex b₄ being strict Subalgebra of b₂ st the carrier of b₄ = b₃

proof end;

theorem Th21: :: POLYALG1:21

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being non empty Subset of b₂
for b₄ being Subset-Family of b₂ st ( for b₅ being set holds
( b₅ in b₄ iff ( b₅ c= the carrier of b₂ & ex b₆ being Subalgebra of b₂ st
( b₅ = the carrier of b₆ & b₃ c= b₅ ) ) ) ) holds
meet b₄ is opers_closed

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂ be non empty AlgebraStr of c₁;
let c₃ be non empty Subset of c₂;
func GenAlg c₃ -> non empty strict Subalgebra of a₂ means :Def5: :: POLYALG1:def 5
( a₃ c= the carrier of a₄ & ( for b₁ being Subalgebra of a₂ st a₃ c= the carrier of b₁ holds
the carrier of a₄ c= the carrier of b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines GenAlg POLYALG1:def 5 :

theorem Th22: :: POLYALG1:22

for b₁ being non empty HGrStr
for b₂ being non empty AlgebraStr of b₁
for b₃ being non empty Subset of b₂ st b₃ is opers_closed holds
the carrier of (GenAlg b₃) = b₃

proof end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
func Polynom-Algebra c₁ -> non empty strict AlgebraStr of a₁ means :Def6: :: POLYALG1:def 6
ex b₁ being non empty Subset of (Formal-Series a₁) st
( b₁ = the carrier of (Polynom-Ring a₁) & a₂ = GenAlg b₁ );
existence

proof end;

uniqueness ;

end;

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

registration

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

proof end;

end;

theorem Th23: :: POLYALG1:23

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂ being non empty Subset of (Formal-Series b₁) st b₂ = the carrier of (Polynom-Ring b₁) holds
b₂ is opers_closed

proof end;

theorem Th24: :: POLYALG1:24

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

proof end;

theorem Th25: :: POLYALG1:25

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