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

begin

theorem :: POLYNOM4:1

canceled;

theorem :: POLYNOM4:2

canceled;

theorem :: POLYNOM4:3

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:87;

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 associative commutative right-distributive well-unital left_zeroed -> non empty right_add-cancelable associative commutative right-distributive well-unital domRing-like left_zeroed doubleLoopStr ;
coherence
for b₁ being non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr st b₁ is almost_left_invertible holds
b₁ is domRing-like

proof end;

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 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 & not b₁ is trivial )

proof end;

end;

begin

theorem :: POLYNOM4:4

canceled;

theorem Th5: :: POLYNOM4:5

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 Th6: :: POLYNOM4:6

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

proof end;

theorem Th7: :: POLYNOM4:7

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

proof end;

theorem Th8: :: POLYNOM4:8

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

proof end;

theorem Th9: :: POLYNOM4:9

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 Th10: :: POLYNOM4:10

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 Th11: :: POLYNOM4:11

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:12

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:13

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

proof end;

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) & ( 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 Th14: :: POLYNOM4:14

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 Th15: :: POLYNOM4:15

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:16

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

proof end;

theorem :: POLYNOM4:17

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

proof end;

theorem Th18: :: POLYNOM4:18

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

proof end;

theorem Th19: :: POLYNOM4:19

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;

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 & 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 Th20: :: POLYNOM4:20

for L being non empty unital doubleLoopStr
for x being Element of L holds eval ((0_. L),x) = 0. L

proof end;

theorem Th21: :: POLYNOM4:21

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

proof end;

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

proof end;

theorem Th22: :: POLYNOM4:22

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

proof end;

theorem Th23: :: POLYNOM4:23

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

proof end;

theorem :: POLYNOM4:24

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

proof end;

theorem Th25: :: POLYNOM4:25

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

proof end;

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 & 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;

Lm4: for L being non empty 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))

proof end;

theorem Th26: :: POLYNOM4:26

for L being non empty 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))

proof end;

theorem Th27: :: POLYNOM4:27

for L being non empty 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))

proof end;

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 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 unital distributive 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 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

proof end;

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

proof end;

end;

registration

let L be non empty 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

proof end;

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

proof end;

end;