begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
begin
:: deftheorem Def1 defines < POLYNOM3:def 1 :
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p < q iff ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k ) ) );
:: deftheorem Def2 defines <= POLYNOM3:def 2 :
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q iff ( p < q or p = q ) );
theorem Th5:
theorem Th6:
theorem Th7:
:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
for n being Element of NAT
for b2 being Order of (n -tuples_on NAT) holds
( b2 = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) );
begin
:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
for i being non empty Element of NAT
for n being Element of NAT
for b3 being FinSequence of i -tuples_on NAT holds
( b3 = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st
( b3 = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for b6 being Element of the carrier of L * holds
( b6 = prodTuples (p,q,r,t) iff ( len b6 = len t & ( for k being Element of NAT st k in dom t holds
b6 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) ) );
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
begin
theorem Th23:
theorem Th24:
theorem
theorem Th26:
Lm1:
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)
:: deftheorem POLYNOM3:def 6 :
canceled;
:: deftheorem POLYNOM3:def 7 :
canceled;
:: deftheorem defines - POLYNOM3:def 8 :
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q);
theorem
:: deftheorem defines 0_. POLYNOM3:def 9 :
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);
theorem
canceled;
theorem Th29:
theorem Th30:
:: deftheorem defines 1_. POLYNOM3:def 10 :
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));
theorem Th31:
:: deftheorem Def11 defines *' POLYNOM3:def 11 :
for L being non empty doubleLoopStr
for p, q, b4 being sequence of L holds
( b4 = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b4 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
begin
definition
let L be non
empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
func Polynom-Ring L -> non
empty strict doubleLoopStr means :
Def12:
( ( for
x being
set holds
(
x in the
carrier of
it iff
x is
Polynomial 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 ) &
0. it = 0_. L &
1. it = 1_. L );
existence
ex b1 being non empty strict doubleLoopStr st
( ( for x being set holds
( x in the carrier of b1 iff x is Polynomial 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 ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
uniqueness
for b1, b2 being non empty strict doubleLoopStr st ( for x being set holds
( x in the carrier of b1 iff x is Polynomial 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 ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is Polynomial 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 ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
end;
:: deftheorem Def12 defines Polynom-Ring POLYNOM3:def 12 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for b2 being non empty strict doubleLoopStr holds
( b2 = Polynom-Ring L iff ( ( for x being set holds
( x in the carrier of b2 iff x is Polynomial 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 ) & 0. b2 = 0_. L & 1. b2 = 1_. L ) );
theorem