begin
:: deftheorem defines mix-associative POLYALG1:def 1 :
for L being non empty doubleLoopStr
for A being non empty AlgebraStr of 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 );
theorem Th1:
theorem Th2:
begin
definition
let L be non
empty doubleLoopStr ;
func Formal-Series L -> non
empty strict AlgebraStr of
L means :
Def2:
( ( 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 of 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 )
uniqueness
for b1, b2 being non empty strict AlgebraStr of 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
end;
:: deftheorem Def2 defines Formal-Series POLYALG1:def 2 :
for L being non empty doubleLoopStr
for b2 being non empty strict AlgebraStr of 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 ) );
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
consider D00 being non empty right_complementable associative distributive add-associative right_zeroed doubleLoopStr ;
theorem Th10:
:: deftheorem Def3 defines Subalgebra POLYALG1:def 3 :
for L being 1-sorted
for A, b3 being AlgebraStr of 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:
theorem
theorem
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
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 #)
theorem Th14:
for
L being
1-sorted for
A,
B being
AlgebraStr of
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
:: deftheorem Def4 defines opers_closed POLYALG1:def 4 :
for L being non empty multMagma
for B being non empty AlgebraStr of 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:
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
theorem Th20:
theorem Th21:
:: deftheorem Def5 defines GenAlg POLYALG1:def 5 :
for L being non empty multMagma
for B being non empty AlgebraStr of 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 Th22:
begin
:: 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 of 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 ) );
theorem Th23:
theorem
theorem