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

theorem :: POLYNOM4:1

for D being non empty set
for p being FinSequence of D
for n being Element of NAT st 1 <= n & 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

proof end;

registration

cluster non empty right_add-cancelable almost_left_invertible right-distributive well-unital associative left_zeroed -> non empty right_add-cancelable right-distributive well-unital associative domRing-like left_zeroed for doubleLoopStr ;

coherence
for b₁ being non empty right_add-cancelable right-distributive well-unital associative left_zeroed doubleLoopStr st b₁ is almost_left_invertible holds
b₁ is domRing-like

proof end;

end;

registration

cluster non empty non degenerated right_complementable almost_left_invertible strict Abelian add-associative right_zeroed distributive unital associative commutative domRing-like for doubleLoopStr ;

existence
ex b₁ being non empty doubleLoopStr st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is associative & b₁ is commutative & b₁ is distributive & b₁ is unital & b₁ is domRing-like & b₁ is almost_left_invertible & not b₁ is degenerated )

proof end;

end;

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

proof end;

theorem Th3: :: POLYNOM4:3

for L being non empty ZeroStr holds len (0_. L) = 0

proof end;

theorem Th4: :: POLYNOM4:4

for L being non empty non degenerated multLoopStr_0 holds len (1_. L) = 1

proof end;

theorem Th5: :: POLYNOM4:5

for L being non empty ZeroStr
for p being Polynomial of L st len p = 0 holds
p = 0_. L

proof end;

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 & n >= len q holds
n >= len (p + q)

proof end;

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))

proof end;

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

proof end;

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 & n >= len q holds
n >= len (p - q)

proof end;

theorem :: POLYNOM4:10

for L being non empty right_complementable add-associative right_zeroed distributive left_unital associative 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

proof end;

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) & ( for n being Element of NAT st n <> (len p) -' 1 holds
it . n = 0. L ) );

existence
ex b₁ being sequence of L st
( b₁ . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
b₁ . n = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being sequence of L st b₁ . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
b₁ . n = 0. L ) & b₂ . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
b₂ . n = 0. L ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def 1 :
for L being non empty ZeroStr
for p being Polynomial of L
for b₃ being sequence of L holds
( b₃ = Leading-Monomial p iff ( b₃ . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
b₃ . 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)))

proof end;

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

proof end;

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

proof end;

theorem :: POLYNOM4:13

for L being non empty ZeroStr holds Leading-Monomial (0_. L) = 0_. L

proof end;

theorem :: POLYNOM4:14

for L being non empty non degenerated multLoopStr_0 holds Leading-Monomial (1_. L) = 1_. L

proof end;

theorem Th15: :: POLYNOM4:15

for L being non empty ZeroStr
for p being Polynomial of L holds len (Leading-Monomial p) = len p

proof end;

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 & p = q + (Leading-Monomial p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) )

proof end;

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 & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) );

existence
ex b₁ being Element of L ex F being FinSequence of the carrier of L st
( b₁ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) )

proof end;

uniqueness
for b₁, b₂ being Element of L st ex F being FinSequence of the carrier of L st
( b₁ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) & ex F being FinSequence of the carrier of L st
( b₂ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines eval POLYNOM4:def 2 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x, b₄ being Element of L holds
( b₄ = eval (p,x) iff ex F being FinSequence of the carrier of L st
( b₄ = Sum F & len F = len p & ( 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

proof end;

theorem Th18: :: POLYNOM4:18

for L being non empty non degenerated right_complementable add-associative right_zeroed well-unital associative doubleLoopStr
for x being Element of L holds eval ((1_. L),x) = 1. L

proof end;

theorem Th19: :: POLYNOM4:19

for L being non empty right_complementable Abelian add-associative right_zeroed left-distributive 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))

proof end;

theorem Th20: :: POLYNOM4:20

for L being non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds eval ((- p),x) = - (eval (p,x))

proof end;

theorem :: POLYNOM4:21

for L being non empty right_complementable Abelian add-associative right_zeroed distributive 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))

proof end;

theorem Th22: :: POLYNOM4:22

for L being non empty right_complementable add-associative right_zeroed distributive unital 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)))

proof end;

Lm2: for L being non empty right_complementable add-associative right_zeroed distributive unital associative doubleLoopStr
for p, q being Polynomial of L st len p > 0 & 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)))

proof end;

Lm3: for L being non trivial right_complementable add-associative right_zeroed distributive left_unital associative commutative 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))

proof end;

theorem Th23: :: POLYNOM4:23

for L being non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative 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))

proof end;

theorem Th24: :: POLYNOM4:24

for L being non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative 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))

proof end;

definition

let L be non empty right_complementable add-associative right_zeroed distributive unital 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 b₁ being Function of (Polynom-Ring L),L st
for p being Polynomial of L holds b₁ . p = eval (p,x)

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring L),L st ( for p being Polynomial of L holds b₁ . p = eval (p,x) ) & ( for p being Polynomial of L holds b₂ . p = eval (p,x) ) holds
b₁ = b₂

proof end;

end;

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

registration

let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let x be Element of L;

cluster Polynom-Evaluation (L,x) -> unity-preserving ;

coherence
Polynom-Evaluation (L,x) is unity-preserving

proof end;

end;

registration

let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ;
let x be Element of L;

cluster Polynom-Evaluation (L,x) -> additive ;

coherence
Polynom-Evaluation (L,x) is additive

proof end;

end;

registration

let L be non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr ;
let x be Element of L;

cluster Polynom-Evaluation (L,x) -> multiplicative ;

coherence
Polynom-Evaluation (L,x) is multiplicative

proof end;

end;

registration

let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;
let x be Element of L;

cluster Polynom-Evaluation (L,x) -> RingHomomorphism ;

coherence
Polynom-Evaluation (L,x) is RingHomomorphism ;

end;