:: POLYNOM4 semantic presentation

Lemma1: for b₁ being Nat holds 0 -' b₁ = 0
by NAT_2:10;

theorem Th1: :: POLYNOM4:1

canceled;

theorem Th2: :: POLYNOM4:2

canceled;

theorem Th3: :: POLYNOM4:3

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
b₂ = ((b₂ | (b₃ -' 1)) ^ <*(b₂ . b₃)*>) ^ (b₂ /^ b₃)

proof end;

Lemma3: for b₁ being non empty right-distributive left_zeroed add-right-cancelable doubleLoopStr
for b₂ being Element of b₁ holds b₂ * (0. b₁) = 0. b₁

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 Th4: :: POLYNOM4:4

canceled;

theorem Th5: :: POLYNOM4:5

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂ being sequence of b₁ holds (0_. b₁) *' b₂ = 0_. b₁

proof end;

theorem Th6: :: POLYNOM4:6

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

proof end;

theorem Th7: :: POLYNOM4:7

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

proof end;

theorem Th8: :: POLYNOM4:8

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ st len b₂ = 0 holds
b₂ = 0_. b₁

proof end;

theorem Th9: :: POLYNOM4:9

for b₁ being non empty right_zeroed LoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Nat st b₄ >= len b₂ & b₄ >= len b₃ holds
b₄ >= len (b₂ + b₃)

proof end;

theorem Th10: :: POLYNOM4:10

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Polynomial of b₁ st len b₂ <> len b₃ holds
len (b₂ + b₃) = max (len b₂),(len b₃)

proof end;

theorem Th11: :: POLYNOM4:11

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Polynomial of b₁ holds len (- b₂) = len b₂

proof end;

theorem Th12: :: POLYNOM4:12

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Nat st b₄ >= len b₂ & b₄ >= len b₃ holds
b₄ >= len (b₂ - b₃)

proof end;

theorem Th13: :: POLYNOM4:13

for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st (b₂ . ((len b₂) -' 1)) * (b₃ . ((len b₃) -' 1)) <> 0. b₁ holds
len (b₂ *' b₃) = ((len b₂) + (len b₃)) - 1

proof end;

definition

let c₁ be non empty ZeroStr ;
let c₂ be Polynomial of c₁;
func Leading-Monomial c₂ -> sequence of a₁ means :Def1: :: POLYNOM4:def 1
( a₃ . ((len a₂) -' 1) = a₂ . ((len a₂) -' 1) & ( for b₁ being Nat st b₁ <> (len a₂) -' 1 holds
a₃ . b₁ = 0. a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th14: :: POLYNOM4:14

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ holds Leading-Monomial b₂ = (0_. b₁) +* ((len b₂) -' 1),(b₂ . ((len b₂) -' 1))

proof end;

registration

let c₁ be non empty ZeroStr ;
let c₂ be Polynomial of c₁;
cluster Leading-Monomial a₂ -> finite-Support ;
coherence

proof end;

end;

theorem Th15: :: POLYNOM4:15

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ st len b₂ = 0 holds
Leading-Monomial b₂ = 0_. b₁

proof end;

theorem Th16: :: POLYNOM4:16

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

proof end;

theorem Th17: :: POLYNOM4:17

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

proof end;

theorem Th18: :: POLYNOM4:18

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁ holds len (Leading-Monomial b₂) = len b₂

proof end;

theorem Th19: :: POLYNOM4:19

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being Polynomial of b₁ st len b₂ <> 0 holds
ex b₃ being Polynomial of b₁ st
( len b₃ < len b₂ & b₂ = b₃ + (Leading-Monomial b₂) & ( for b₄ being Nat st b₄ < (len b₂) - 1 holds
b₃ . b₄ = b₂ . b₄ ) )

proof end;

definition

let c₁ be non empty unital doubleLoopStr ;
let c₂ be Polynomial of c₁;
let c₃ be Element of c₁;
func eval c₂,c₃ -> Element of a₁ means :Def2: :: POLYNOM4:def 2
ex b₁ being FinSequence of the carrier of a₁ st
( a₄ = Sum b₁ & len b₁ = len a₂ & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = (a₂ . (b₂ -' 1)) * ((power a₁) . a₃,(b₂ -' 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines eval POLYNOM4:def 2 :

theorem Th20: :: POLYNOM4:20

for b₁ being non empty unital doubleLoopStr
for b₂ being Element of b₁ holds eval (0_. b₁),b₂ = 0. b₁

proof end;

theorem Th21: :: POLYNOM4:21

for b₁ being non empty add-associative right_zeroed right_complementable unital associative non degenerated doubleLoopStr
for b₂ being Element of b₁ holds eval (1_. b₁),b₂ = 1. b₁

proof end;

Lemma19: for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂ being Element of b₁ holds (0. b₁) * b₂ = 0. b₁

proof end;

theorem Th22: :: POLYNOM4:22

for b₁ being non empty Abelian add-associative right_zeroed right_complementable unital left-distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval (b₂ + b₃),b₄ = (eval b₂,b₄) + (eval b₃,b₄)

proof end;

theorem Th23: :: POLYNOM4:23

for b₁ being non empty Abelian add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Element of b₁ holds eval (- b₂),b₃ = - (eval b₂,b₃)

proof end;

theorem Th24: :: POLYNOM4:24

for b₁ being non empty Abelian add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval (b₂ - b₃),b₄ = (eval b₂,b₄) - (eval b₃,b₄)

proof end;

theorem Th25: :: POLYNOM4:25

for b₁ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₂ being Polynomial of b₁
for b₃ being Element of b₁ holds eval (Leading-Monomial b₂),b₃ = (b₂ . ((len b₂) -' 1)) * ((power b₁) . b₃,((len b₂) -' 1))

proof end;

Lemma23: for b₁ being non empty add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr
for b₂, b₃ being Polynomial of b₁ st len b₂ > 0 & len b₃ > 0 holds
for b₄ being Element of b₁ holds eval ((Leading-Monomial b₂) *' (Leading-Monomial b₃)),b₄ = ((b₂ . ((len b₂) -' 1)) * (b₃ . ((len b₃) -' 1))) * ((power b₁) . b₄,(((len b₂) + (len b₃)) -' 2))

proof end;

Lemma24: for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital non trivial doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval ((Leading-Monomial b₂) *' (Leading-Monomial b₃)),b₄ = (eval (Leading-Monomial b₂),b₄) * (eval (Leading-Monomial b₃),b₄)

proof end;

theorem Th26: :: POLYNOM4:26

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital non trivial doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval ((Leading-Monomial b₂) *' b₃),b₄ = (eval (Leading-Monomial b₂),b₄) * (eval b₃,b₄)

proof end;

theorem Th27: :: POLYNOM4:27

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital non trivial doubleLoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Element of b₁ holds eval (b₂ *' b₃),b₄ = (eval b₂,b₄) * (eval b₃,b₄)

proof end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let c₂ be Element of c₁;
func Polynom-Evaluation c₁,c₂ -> Function of (Polynom-Ring a₁),a₁ means :Def3: :: POLYNOM4:def 3
for b₁ being Polynomial of a₁ holds a₃ . b₁ = eval b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

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

registration

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

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable unital distributive doubleLoopStr ;
let c₂ be Element of c₁;
cluster Polynom-Evaluation a₁,a₂ -> additive ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;