:: POLYNOM4 semantic presentation

Lm1: for n being Nat holds 0 -' n = 0
by NAT_2:10;

theorem :: POLYNOM4:1

canceled;

theorem :: POLYNOM4:2

canceled;

theorem Th3: :: POLYNOM4:3

for D being non empty set
for p being FinSequence of D
for n being Nat st 1 <= n & n <= len p holds
p = ((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n)

proof end;

Lm2: for R being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R

proof end;

registration

cluster non empty associative commutative right-distributive left_unital Field-like left_zeroed add-right-cancelable -> non empty associative commutative right-distributive left_unital domRing-like left_zeroed add-right-cancelable doubleLoopStr ;
coherence

proof end;

end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non degenerated domRing-like non trivial doubleLoopStr ;
existence

proof end;

end;

theorem :: POLYNOM4:4

canceled;

theorem Th5: :: POLYNOM4:5

for L being non empty add-associative right_zeroed right_complementable 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 LoopStr
for p, q being Polynomial of L
for n being Nat st n >= len p & n >= len q holds
n >= len (p + q)

proof end;

theorem Th10: :: POLYNOM4:10

for L being non empty add-associative right_zeroed right_complementable LoopStr
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 add-associative right_zeroed right_complementable LoopStr
for p being Polynomial of L holds len (- p) = len p

proof end;

theorem :: POLYNOM4:12

for L being non empty add-associative right_zeroed right_complementable LoopStr
for p, q being Polynomial of L
for n being Nat st n >= len p & n >= len q holds
n >= len (p - q)

proof end;

theorem :: POLYNOM4:13

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

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 Nat st n <> (len p) -' 1 holds
it . n = 0. L ) );
existence

proof end;

uniqueness

proof end;

end;

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

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

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 add-associative right_zeroed right_complementable LoopStr
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 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 Nat st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . x,(n -' 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines eval POLYNOM4:def 2 :

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 add-associative right_zeroed right_complementable unital associative non degenerated doubleLoopStr
for x being Element of L holds eval (1_. L),x = 1. L

proof end;

Lm3: for F being non empty add-associative right_zeroed right_complementable 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 Abelian add-associative right_zeroed right_complementable 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 Abelian add-associative right_zeroed right_complementable 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 Abelian add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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;

Lm4: for L being non empty add-associative right_zeroed right_complementable 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;

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

proof end;

definition

let L be non empty add-associative right_zeroed right_complementable 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def 3 :

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

let L be non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital non trivial doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation L,x -> additive multiplicative ;
coherence

proof end;

end;

registration

let L be non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital non degenerated doubleLoopStr ;
let x be Element of L;
cluster Polynom-Evaluation L,x -> RingHomomorphism additive unity-preserving multiplicative ;
coherence

proof end;

end;