:: by Robert Milewski

::

:: Received June 7, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

theorem :: POLYNOM4:1

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

for b_{1} being non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr st b_{1} is almost_left_invertible holds

b_{1} is domRing-like
end;

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 b

b

proof end;

registration

ex b_{1} being non trivial doubleLoopStr st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is associative & b_{1} is commutative & b_{1} is distributive & b_{1} is unital & b_{1} is domRing-like & b_{1} is almost_left_invertible & not b_{1} is degenerated )
end;

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 b

( b

proof 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

for p being sequence of L holds (0_. L) *' 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)

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

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

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)

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

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;

ex b_{1} being sequence of L st

( b_{1} . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds

b_{1} . n = 0. L ) )

for b_{1}, b_{2} being sequence of L st b_{1} . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds

b_{1} . n = 0. L ) & b_{2} . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds

b_{2} . n = 0. L ) holds

b_{1} = b_{2}

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

it . n = 0. L ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Leading-Monomial POLYNOM4:def 1 :

for L being non empty ZeroStr

for p being Polynomial of L

for b_{3} being sequence of L holds

( b_{3} = Leading-Monomial p iff ( b_{3} . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds

b_{3} . n = 0. L ) ) );

for L being non empty ZeroStr

for p being Polynomial of L

for b

( b

b

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

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;

coherence

Leading-Monomial p is finite-Support

end;
let p be Polynomial of L;

coherence

Leading-Monomial p is finite-Support

proof 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

for p being Polynomial of L st len p = 0 holds

Leading-Monomial p = 0_. L

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

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;

ex b_{1} being Element of L ex F being FinSequence of the carrier of L st

( b_{1} = 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))) ) )

for b_{1}, b_{2} being Element of L st ex F being FinSequence of the carrier of L st

( b_{1} = 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_{2} = 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_{1} = b_{2}

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

ex b

( b

F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) )

proof end;

uniqueness for b

( b

F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) & ex F being FinSequence of the carrier of L st

( b

F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) holds

b

proof end;

:: deftheorem Def2 defines eval POLYNOM4:def 2 :

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for x, b_{4} being Element of L holds

( b_{4} = eval (p,x) iff ex F being FinSequence of the carrier of L st

( b_{4} = 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))) ) ) );

for L being non empty unital doubleLoopStr

for p being Polynomial of L

for x, b

( b

( b

F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) );

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

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

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

for p being Polynomial of L

for x being Element of L holds eval ((- p),x) = - (eval (p,x))

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

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

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

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

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;

ex b_{1} being Function of (Polynom-Ring L),L st

for p being Polynomial of L holds b_{1} . p = eval (p,x)

for b_{1}, b_{2} being Function of (Polynom-Ring L),L st ( for p being Polynomial of L holds b_{1} . p = eval (p,x) ) & ( for p being Polynomial of L holds b_{2} . p = eval (p,x) ) holds

b_{1} = b_{2}

end;
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 for p being Polynomial of L holds it . p = eval (p,x);

ex b

for p being Polynomial of L holds b

proof end;

uniqueness for b

b

proof 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_{3} being Function of (Polynom-Ring L),L holds

( b_{3} = Polynom-Evaluation (L,x) iff for p being Polynomial of L holds b_{3} . p = eval (p,x) );

for L being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr

for x being Element of L

for b

( b

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;

coherence

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

end;
let x be Element of L;

coherence

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

proof end;

registration

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

let x be Element of L;

coherence

Polynom-Evaluation (L,x) is additive

end;
let x be Element of L;

coherence

Polynom-Evaluation (L,x) is additive

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

coherence

Polynom-Evaluation (L,x) is multiplicative

end;
let x be Element of L;

coherence

Polynom-Evaluation (L,x) is multiplicative

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

coherence

Polynom-Evaluation (L,x) is RingHomomorphism

end;
let x be Element of L;

coherence

Polynom-Evaluation (L,x) is RingHomomorphism

proof end;