:: Evaluation of Polynomials
:: by Robert Milewski
::
:: Received June 7, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem :: POLYNOM4:1
for D being non empty set
for p being FinSequence of D
for n being Element of NAT st 1 <= n &amp; n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n) by FINSEQ_5:84;

Lm1:  for R being non empty right_add-cancelable right-distributive left_zeroed doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R
proofend;

registration
cluster non empty right_add-cancelable almost_left_invertible associative commutative right-distributive well-unital left_zeroed  ->  non empty right_add-cancelable associative commutative right-distributive well-unital domRing-like left_zeroed for doubleLoopStr ;
coherence
 for b1 being non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr st b1 is almost_left_invertible holds
b1 is domRing-like
proofend;
end;

registration
cluster non empty non degenerated non trivial right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative distributive domRing-like for doubleLoopStr ;
existence
 ex b1 being non trivial doubleLoopStr st
( b1 is strict &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is associative &amp; b1 is commutative &amp; b1 is distributive &amp; b1 is unital &amp; b1 is domRing-like &amp; b1 is almost_left_invertible &amp; not b1 is degenerated )
proofend;
end;

begin

theorem Th2: :: POLYNOM4:2
for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being sequence of L holds (0_. L) *' p = 0_. L
proofend;

theorem Th3: :: POLYNOM4:3
for L being non empty ZeroStr holds len (0_. L) = 0
proofend;

theorem Th4: :: POLYNOM4:4
for L being non empty non degenerated multLoopStr_0 holds len (1_. L) = 1
proofend;

theorem Th5: :: POLYNOM4:5
for L being non empty ZeroStr
for p being Polynomial of L st len p = 0 holds
p = 0_. L
proofend;

theorem Th6: :: POLYNOM4:6
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n >= len p &amp; n >= len q holds
n >= len (p + q)
proofend;

theorem Th7: :: POLYNOM4:7
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st len p <> len q holds
len (p + q) = max ((len p),(len q))
proofend;

theorem Th8: :: POLYNOM4:8
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds len (- p) = len p
proofend;

theorem :: POLYNOM4:9
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L
for n being Element of NAT st n >= len p &amp; n >= len q holds
n >= len (p - q)
proofend;

theorem :: POLYNOM4:10
for L being non empty right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
len (p *' q) = ((len p) + (len q)) - 1
proofend;

begin

definition
let L be non empty ZeroStr ;
let p be Polynomial of L;
func Leading-Monomial p ->  sequence of L means :Def1: :: POLYNOM4:def 1
( it . ((len p) -' 1) = p . ((len p) -' 1) &amp; ( for n being Element of NAT st n <> (len p) -' 1 holds
it . n = 0. L ) );
existence
 ex b1 being sequence of L st
( b1 . ((len p) -' 1) = p . ((len p) -' 1) &amp; ( for n being Element of NAT st n <> (len p) -' 1 holds
b1 . n = 0. L ) )
proofend;
uniqueness
 for b1, b2 being sequence of L st b1 . ((len p) -' 1) = p . ((len p) -' 1) &amp; ( for n being Element of NAT st n <> (len p) -' 1 holds
b1 . n = 0. L ) &amp; b2 . ((len p) -' 1) = p . ((len p) -' 1) &amp; ( for n being Element of NAT st n <> (len p) -' 1 holds
b2 . n = 0. L ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def_1_:_
 for L being non empty ZeroStr
for p being Polynomial of L
for b3 being sequence of L holds
( b3 = Leading-Monomial p iff ( b3 . ((len p) -' 1) = p . ((len p) -' 1) &amp; ( for n being Element of NAT st n <> (len p) -' 1 holds
b3 . n = 0. L ) ) );

theorem Th11: :: POLYNOM4:11
for L being non empty ZeroStr
for p being Polynomial of L holds Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1)))
proofend;

registration
let L be non empty ZeroStr ;
let p be Polynomial of L;
cluster Leading-Monomial p ->  finite-Support ;
coherence
 Leading-Monomial p is finite-Support
proofend;
end;

theorem Th12: :: POLYNOM4:12
for L being non empty ZeroStr
for p being Polynomial of L st len p = 0 holds
Leading-Monomial p = 0_. L
proofend;

theorem :: POLYNOM4:13
for L being non empty ZeroStr holds Leading-Monomial (0_. L) = 0_. L
proofend;

theorem :: POLYNOM4:14
for L being non empty non degenerated multLoopStr_0 holds Leading-Monomial (1_. L) = 1_. L
proofend;

theorem Th15: :: POLYNOM4:15
for L being non empty ZeroStr
for p being Polynomial of L holds len (Leading-Monomial p) = len p
proofend;

theorem Th16: :: POLYNOM4:16
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L st len p <> 0 holds
ex q being Polynomial of L st
( len q < len p &amp; p = q + (Leading-Monomial p) &amp; ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )
proofend;

begin

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
func eval (p,x) ->  Element of L means :Def2: :: POLYNOM4:def 2
 ex F being FinSequence of the carrier of L st
( it = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) );
existence
 ex b1 being Element of L ex F being FinSequence of the carrier of L st
( b1 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) )
proofend;
uniqueness
 for b1, b2 being Element of L st ex F being FinSequence of the carrier of L st
( b1 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) &amp; ex F being FinSequence of the carrier of L st
( b2 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines eval POLYNOM4:def_2_:_
 for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x, b4 being Element of L holds
( b4 = eval (p,x) iff ex F being FinSequence of the carrier of L st
( b4 = Sum F &amp; len F = len p &amp; ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) );

theorem Th17: :: POLYNOM4:17
for L being non empty unital doubleLoopStr
for x being Element of L holds eval ((0_. L),x) = 0. L
proofend;

theorem Th18: :: POLYNOM4:18
for L being non empty non degenerated right_complementable add-associative right_zeroed associative well-unital doubleLoopStr
for x being Element of L holds eval ((1_. L),x) = 1. L
proofend;

Lm2:  for F being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for x being Element of F holds (0. F) * x = 0. F
proofend;

theorem Th19: :: POLYNOM4:19
for L being non empty right_complementable Abelian add-associative right_zeroed unital left-distributive doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))
proofend;

theorem Th20: :: POLYNOM4:20
for L being non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr
for p being Polynomial of L
for x being Element of L holds eval ((- p),x) = - (eval (p,x))
proofend;

theorem :: POLYNOM4:21
for L being non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((p - q),x) = (eval (p,x)) - (eval (q,x))
proofend;

theorem Th22: :: POLYNOM4:22
for L being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr
for p being Polynomial of L
for x being Element of L holds eval ((Leading-Monomial p),x) = (p . ((len p) -' 1)) * ((power L) . (x,((len p) -' 1)))
proofend;

Lm3:  for L being non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr
for p, q being Polynomial of L st len p > 0 &amp; len q > 0 holds
for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2)))
proofend;

Lm4:  for L being non trivial right_complementable add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (eval ((Leading-Monomial p),x)) * (eval ((Leading-Monomial q),x))
proofend;

theorem Th23: :: POLYNOM4:23
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval (((Leading-Monomial p) *' q),x) = (eval ((Leading-Monomial p),x)) * (eval (q,x))
proofend;

theorem Th24: :: POLYNOM4:24
for L being non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))
proofend;

begin

definition
let L be non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr ;
let x be Element of L;
func Polynom-Evaluation (L,x) ->  Function of (Polynom-Ring L),L means :Def3: :: POLYNOM4:def 3
 for p being Polynomial of L holds it . p = eval (p,x);
existence
 ex b1 being Function of (Polynom-Ring L),L st
for p being Polynomial of L holds b1 . p = eval (p,x)
proofend;
uniqueness
 for b1, b2 being Function of (Polynom-Ring L),L st ( for p being Polynomial of L holds b1 . p = eval (p,x) ) &amp; ( for p being Polynomial of L holds b2 . p = eval (p,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def_3_:_
 for L being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr
for x being Element of L
for b3 being Function of (Polynom-Ring L),L holds
( b3 = Polynom-Evaluation (L,x) iff for p being Polynomial of L holds b3 . p = eval (p,x) );

registration
let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation (L,x) ->  unity-preserving ;
coherence
 Polynom-Evaluation (L,x) is unity-preserving
proofend;
end;

registration
let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation (L,x) ->  additive ;
coherence
 Polynom-Evaluation (L,x) is additive
proofend;
end;

registration
let L be non trivial right_complementable Abelian add-associative right_zeroed associative commutative distributive left_unital doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation (L,x) ->  multiplicative ;
coherence
 Polynom-Evaluation (L,x) is multiplicative
proofend;
end;

registration
let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation (L,x) ->  RingHomomorphism ;
coherence
 Polynom-Evaluation (L,x) is RingHomomorphism
proofend;
end;