:: The Ring of Polynomials
:: by Robert Milewski
::
:: Received April 17, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: POLYNOM3:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of L st ( for i being Element of NAT st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L
proof end;

theorem Th2: :: POLYNOM3:2
for V being non empty Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of V holds Sum p = Sum (Rev p)
proof end;

theorem Th3: :: POLYNOM3:3
for p being FinSequence of REAL holds Sum p = Sum (Rev p)
proof end;

theorem Th4: :: POLYNOM3:4
for p being FinSequence of NAT
for i being Element of NAT st i in dom p holds
Sum p >= p . i
proof end;

definition
let D be non empty set ;
let i be Element of NAT ;
let p be FinSequence of D;
:: original: Del
redefine func Del (p,i) -> FinSequence of D;
coherence
Del (p,i) is FinSequence of D
by FINSEQ_3:105;
end;

definition
let D be non empty set ;
let a, b be Element of D;
:: original: <*
redefine func <*a,b*> -> Element of 2 -tuples_on D;
coherence
<*a,b*> is Element of 2 -tuples_on D
by FINSEQ_2:101;
end;

definition
let D be non empty set ;
let k, n be Element of NAT ;
let p be Element of k -tuples_on D;
let q be Element of n -tuples_on D;
:: original: ^
redefine func p ^ q -> Element of (k + n) -tuples_on D;
coherence
p ^ q is Element of (k + n) -tuples_on D
proof end;
end;

definition
let D be non empty set ;
let k, n be Nat;
let p be FinSequence of k -tuples_on D;
let q be FinSequence of n -tuples_on D;
:: original: ^^
redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;
coherence
p ^^ q is Element of ((k + n) -tuples_on D) *
proof end;
end;

scheme :: POLYNOM3:sch 1
SeqOfSeqLambdaD{ F1() -> non empty set , F2() -> Element of NAT , F3( Nat) -> Element of NAT , F4( set , set ) -> Element of F1() } :
ex p being FinSequence of F1() * st
( len p = F2() & ( for k being Element of NAT st k in Seg F2() holds
( len (p /. k) = F3(k) & ( for n being Element of NAT st n in dom (p /. k) holds
(p /. k) . n = F4(k,n) ) ) ) )
proof end;

definition
let n be Nat;
let p, q be Element of n -tuples_on NAT;
pred p < q means :: POLYNOM3:def 1
ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) );
asymmetry
for p, q being Element of n -tuples_on NAT st ex i being Element of NAT st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) ) holds
for i being Element of NAT holds
( not i in Seg n or not q . i < p . i or ex k being Nat st
( 1 <= k & k < i & not q . k = p . k ) )
proof end;
end;

:: deftheorem defines < POLYNOM3:def 1 :
for n being 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 Nat st 1 <= k & k < i holds
p . k = q . k ) ) );

notation
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q > p for p < q;
end;

definition
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
pred p <= q means :: POLYNOM3:def 2
( p < q or p = q );
reflexivity
for p being Element of n -tuples_on NAT holds
( p < p or p = p )
;
end;

:: deftheorem 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 ) );

notation
let n be Element of NAT ;
let p, q be Element of n -tuples_on NAT;
synonym q >= p for p <= q;
end;

theorem Th5: :: POLYNOM3:5
for n being Element of NAT
for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
proof end;

theorem Th6: :: POLYNOM3:6
for n being Nat
for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Element of NAT st
( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) )
proof end;

theorem Th7: :: POLYNOM3:7
for n being Element of NAT
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )
proof end;

definition
let n be Element of NAT ;
func TuplesOrder n -> Order of () means :Def3: :: POLYNOM3:def 3
for p, q being Element of n -tuples_on NAT holds
( [p,q] in it iff p <= q );
existence
ex b1 being Order of () st
for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q )
proof end;
uniqueness
for b1, b2 being Order of () st ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b1 iff p <= q ) ) & ( for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :
for n being Element of NAT
for b2 being Order of () holds
( b2 = TuplesOrder n iff for p, q being Element of n -tuples_on NAT holds
( [p,q] in b2 iff p <= q ) );

registration
let n be Element of NAT ;
coherence
proof end;
end;

definition
let i be non zero Element of NAT ;
let n be Element of NAT ;
func Decomp (n,i) -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex A being finite Subset of () st
( it = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );
existence
ex b1 being FinSequence of i -tuples_on NAT ex A being finite Subset of () st
( b1 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of i -tuples_on NAT st ex A being finite Subset of () st
( b1 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) & ex A being finite Subset of () st
( b2 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
for i being non zero 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 () st
( b3 = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );

registration
let i be non zero Element of NAT ;
let n be Element of NAT ;
coherence
( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding )
proof end;
end;

theorem Th8: :: POLYNOM3:8
for n being Element of NAT holds len (Decomp (n,1)) = 1
proof end;

theorem Th9: :: POLYNOM3:9
for n being Element of NAT holds len (Decomp (n,2)) = n + 1
proof end;

theorem :: POLYNOM3:10
for n being Element of NAT holds Decomp (n,1) =
proof end;

theorem Th11: :: POLYNOM3:11
for i, j, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )
proof end;

theorem Th12: :: POLYNOM3:12
for i, n, k1, k2 being Element of NAT st (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1
proof end;

theorem Th13: :: POLYNOM3:13
for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*>
proof end;

theorem Th14: :: POLYNOM3:14
for n, i being Element of NAT st i in Seg (n + 1) holds
(Decomp (n,2)) . i = <*(i -' 1),((n + 1) -' i)*>
proof end;

definition
let L be non empty multMagma ;
let p, q, r be sequence of L;
let t be FinSequence of 3 -tuples_on NAT;
func prodTuples (p,q,r,t) -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5
( len it = len t & ( for k being Element of NAT st k in dom t holds
it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );
existence
ex b1 being Element of the carrier of L * st
( len b1 = len t & ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )
proof end;
uniqueness
for b1, b2 being Element of the carrier of L * st len b1 = len t & ( for k being Element of NAT st k in dom t holds
b1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) & len b2 = len t & ( for k being Element of NAT st k in dom t holds
b2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) holds
b1 = b2
proof end;
end;

:: 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: :: POLYNOM3:15
for L being non empty multMagma
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
proof end;

theorem Th16: :: POLYNOM3:16
for D being set
for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i
proof end;

theorem :: POLYNOM3:17
canceled;

::$CT theorem Th17: :: POLYNOM3:18 for p being FinSequence of NAT for i, j being Nat st i <= j holds Sum (p | i) <= Sum (p | j) proof end; theorem :: POLYNOM3:19 canceled; ::$CT
theorem Th19: :: POLYNOM3:20
for p being FinSequence of REAL
for i being Element of NAT st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))
proof end;

theorem Th20: :: POLYNOM3:21
for p being FinSequence of NAT
for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )
proof end;

theorem Th21: :: POLYNOM3:22
for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
proof end;

definition
let L be non empty ZeroStr ;
mode Polynomial of L is AlgSequence of L;
end;

theorem :: POLYNOM3:23
for L being non empty ZeroStr
for p being Polynomial of L
for n being Element of NAT holds
( n >= len p iff n is_at_least_length_of p ) by ;

scheme :: POLYNOM3:sch 2
PolynomialLambdaF{ F1() -> non empty addLoopStr , F2() -> Element of NAT , F3( Element of NAT ) -> Element of F1() } :
ex p being Polynomial of F1() st
( len p <= F2() & ( for n being Element of NAT st n < F2() holds
p . n = F3(n) ) )
proof end;

registration
let L be non empty right_zeroed addLoopStr ;
let p, q be Polynomial of L;
coherence
p + q is finite-Support
proof end;
end;

theorem :: POLYNOM3:24
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q
proof end;

definition
let L be non empty Abelian addLoopStr ;
let p, q be sequence of L;
:: original: +
redefine func p + q -> Element of bool [:NAT, the carrier of L:];
commutativity
for p, q being sequence of L holds p + q = q + p
proof end;
end;

theorem :: POLYNOM3:25
canceled;

::\$CT
theorem Th24: :: POLYNOM3:26
for L being non empty add-associative addLoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)
proof end;

registration
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p be Polynomial of L;
coherence
proof end;
end;

Lm1: for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q)

proof end;

definition
let L be non empty addLoopStr ;
let p, q be sequence of L;
redefine func p - q equals :: POLYNOM3:def 6
p + (- q);
compatibility
for b1 being Element of bool [:NAT, the carrier of L:] holds
( b1 = p - q iff b1 = p + (- q) )
by Lm1;
end;

:: deftheorem defines - POLYNOM3:def 6 :
for L being non empty addLoopStr
for p, q being sequence of L holds p - q = p + (- q);

registration
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of L;
coherence
p - q is finite-Support
;
end;

theorem :: POLYNOM3:27
for L being non empty addLoopStr
for p, q being sequence of L
for n being Element of NAT holds (p - q) . n = (p . n) - (q . n) by NORMSP_1:def 3;

definition
let L be non empty ZeroStr ;
func 0_. L -> sequence of L equals :: POLYNOM3:def 7
NAT --> (0. L);
coherence
NAT --> (0. L) is sequence of L
;
end;

:: deftheorem defines 0_. POLYNOM3:def 7 :
for L being non empty ZeroStr holds 0_. L = NAT --> (0. L);

registration
let L be non empty ZeroStr ;
coherence
proof end;
end;

theorem Th26: :: POLYNOM3:28
for L being non empty right_zeroed addLoopStr
for p being sequence of L holds p + (0_. L) = p
proof end;

theorem Th27: :: POLYNOM3:29
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being sequence of L holds p - p = 0_. L
proof end;

definition
let L be non empty multLoopStr_0 ;
func 1_. L -> sequence of L equals :: POLYNOM3:def 8
(0_. L) +* (0,(1. L));
coherence
(0_. L) +* (0,(1. L)) is sequence of L
;
end;

:: deftheorem defines 1_. POLYNOM3:def 8 :
for L being non empty multLoopStr_0 holds 1_. L = (0_. L) +* (0,(1. L));

registration
let L be non empty multLoopStr_0 ;
coherence
proof end;
end;

theorem Th28: :: POLYNOM3:30
for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
proof end;

definition
let L be non empty doubleLoopStr ;
let p, q be sequence of L;
func p *' q -> sequence of L means :Def9: :: POLYNOM3:def 9
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & it . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );
existence
ex b1 being sequence of L st
for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) )
proof end;
uniqueness
for b1, b2 being sequence of L st ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b1 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) & ( for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b2 . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines *' POLYNOM3:def 9 :
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)) ) ) );

registration
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
let p, q be Polynomial of L;
coherence
p *' q is finite-Support
proof end;
end;

theorem Th29: :: POLYNOM3:31
for L being non empty right_complementable Abelian add-associative right_zeroed right-distributive doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)
proof end;

theorem Th30: :: POLYNOM3:32
for L being non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)
proof end;

theorem Th31: :: POLYNOM3:33
for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)
proof end;

definition
let L be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
let p, q be sequence of L;
:: original: *'
redefine func p *' q -> sequence of L;
commutativity
for p, q being sequence of L holds p *' q = q *' p
proof end;
end;

theorem :: POLYNOM3:34
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being sequence of L holds p *' (0_. L) = 0_. L
proof end;

theorem Th33: :: POLYNOM3:35
for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p
proof end;

definition
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
func Polynom-Ring L -> non empty strict doubleLoopStr means :Def10: :: POLYNOM3:def 10
( ( 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 )
proof end;
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
proof end;
end;

:: deftheorem Def10 defines Polynom-Ring POLYNOM3:def 10 :
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 ) );

registration
let L be non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr ;
coherence
proof end;
end;

registration
let L be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

registration
let L be non empty right_complementable Abelian add-associative right_zeroed distributive commutative doubleLoopStr ;
coherence
proof end;
end;

registration
let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
coherence
proof end;
end;

theorem Th33a: :: POLYNOM3:36
for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p
proof end;

Lm2: now :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for x, e being Element of () st e = 1. () holds
( x * e = x & e * x = x )
let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for x, e being Element of () st e = 1. () holds
( x * e = x & e * x = x )

set Pm = Polynom-Ring L;
let x, e be Element of (); :: thesis: ( e = 1. () implies ( x * e = x & e * x = x ) )
reconsider p = x as Polynomial of L by Def10;
assume A1: e = 1. () ; :: thesis: ( x * e = x & e * x = x )
A2: 1. () = 1_. L by Def10;
hence x * e = p *' (1_. L) by
.= x by Th33 ;
:: thesis: e * x = x
thus e * x = (1_. L) *' p by
.= x by Th33a ; :: thesis: verum
end;

registration
let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;
coherence by Lm2;
end;

registration
let L be non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr ;
coherence
proof end;
end;

theorem :: POLYNOM3:37