:: POLYNOM2 semantic presentation

scheme :: POLYNOM2:sch 1
s1{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex b₁ being FinSequence of F₁() st
( dom b₁ = Seg F₂() & ( for b₂ being Nat st b₂ in Seg F₂() holds
P₁[b₂,b₁ /. b₂] ) )

provided

E1: for b₁ being Nat st b₁ in Seg F₂() holds
ex b₂ being Element of F₁() st P₁[b₁,b₂]

proof end;

scheme :: POLYNOM2:sch 2
s2{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, P₁[ set , set , set ] } :

ex b₁ being FinSequence of F₁() st
( len b₁ = F₃() & ( b₁ /. 1 = F₂() or F₃() = 0 ) & ( for b₂ being Nat st 1 <= b₂ & b₂ <= F₃() - 1 holds
P₁[b₂,b₁ /. b₂,b₁ /. (b₂ + 1)] ) )

provided

E1: for b₁ being Nat st 1 <= b₁ & b₁ <= F₃() - 1 holds
for b₂ being Element of F₁() ex b₃ being Element of F₁() st P₁[b₁,b₂,b₃]

proof end;

scheme :: POLYNOM2:sch 3
s3{ F₁() -> set , F₂() -> Element of F₁(), F₃() -> Nat, F₄() -> FinSequence of F₁(), F₅() -> FinSequence of F₁(), P₁[ set , set , set ] } :

F₄() = F₅()

provided

E1: for b₁ being Nat st 1 <= b₁ & b₁ <= F₃() - 1 holds
for b₂, b₃, b₄ being Element of F₁() st P₁[b₁,b₂,b₃] & P₁[b₁,b₂,b₄] holds
b₃ = b₄ and
E2: ( len F₄() = F₃() & ( F₄() /. 1 = F₂() or F₃() = 0 ) & ( for b₁ being Nat st 1 <= b₁ & b₁ <= F₃() - 1 holds
P₁[b₁,F₄() /. b₁,F₄() /. (b₁ + 1)] ) ) and
E3: ( len F₅() = F₃() & ( F₅() /. 1 = F₂() or F₃() = 0 ) & ( for b₁ being Nat st 1 <= b₁ & b₁ <= F₃() - 1 holds
P₁[b₁,F₅() /. b₁,F₅() /. (b₁ + 1)] ) )

proof end;

scheme :: POLYNOM2:sch 4
s4{ F₁() -> Nat, F₂() -> Nat, P₁[ Nat] } :

for b₁ being Nat st F₁() <= b₁ & b₁ <= F₂() holds
P₁[b₁]

provided

E1: P₁[F₁()] and
E2: for b₁ being Nat st F₁() <= b₁ & b₁ < F₂() & P₁[b₁] holds
P₁[b₁ + 1]

proof end;

scheme :: POLYNOM2:sch 5
s5{ F₁() -> Nat, F₂() -> Nat, P₁[ Nat] } :

for b₁ being Nat st F₁() <= b₁ & b₁ <= F₂() holds
P₁[b₁]

provided

E1: P₁[F₁()] and
E2: for b₁ being Nat st F₁() <= b₁ & b₁ < F₂() & ( for b₂ being Nat st F₁() <= b₂ & b₂ <= b₁ holds
P₁[b₂] ) holds
P₁[b₁ + 1]

proof end;

scheme :: POLYNOM2:sch 6
s6{ F₁() -> set , F₂() -> FinSequence of F₁(), P₁[ set ] } :

for b₁ being Nat st 1 <= b₁ & b₁ <= len F₂() holds
P₁[F₂() . b₁]

provided

E1: P₁[F₂() . 1] and
E2: for b₁ being Nat st 1 <= b₁ & b₁ < len F₂() & P₁[F₂() . b₁] holds
P₁[F₂() . (b₁ + 1)]

proof end;

Lemma1: for b₁ being set
for b₂ being Subset of b₁
for b₃ being Order of b₁ holds
( b₃ is_reflexive_in b₂ & b₃ is_antisymmetric_in b₂ & b₃ is_transitive_in b₂ )

proof end;

Lemma2: for b₁ being set
for b₂ being Subset of b₁
for b₃ being Order of b₁ st b₃ is_connected_in b₁ holds
b₃ is_connected_in b₂

proof end;

Lemma3: for b₁ being set
for b₂ being Subset of b₁
for b₃ being Order of b₁ st b₃ is_linear-order holds
b₃ linearly_orders b₂

proof end;

theorem Th1: :: POLYNOM2:1

canceled;

theorem Th2: :: POLYNOM2:2

for b₁ being non empty unital associative HGrStr
for b₂ being Element of b₁
for b₃, b₄ being Nat holds (power b₁) . b₂,(b₃ + b₄) = ((power b₁) . b₂,b₃) * ((power b₁) . b₂,b₄)

proof end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
existence

proof end;

end;

theorem Th3: :: POLYNOM2:3

canceled;

theorem Th4: :: POLYNOM2:4

for b₁ being FinSequence
for b₂ being Nat st b₂ in dom b₁ holds
for b₃ being Nat st 1 <= b₃ & b₃ <= b₂ holds
b₃ in dom b₁

proof end;

Lemma6: for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Element of b₁
for b₄ being Order of b₁ st b₄ linearly_orders {b₃} \/ b₂ holds
b₄ linearly_orders b₂

proof end;

theorem Th5: :: POLYNOM2:5

for b₁ being non empty right_zeroed left_zeroed LoopStr
for b₂ being FinSequence of the carrier of b₁
for b₃ being Nat st b₃ in dom b₂ & ( for b₄ being Nat st b₄ in dom b₂ & b₄ <> b₃ holds
b₂ /. b₄ = 0. b₁ ) holds
Sum b₂ = b₂ /. b₃

proof end;

theorem Th6: :: POLYNOM2:6

for b₁ being non empty add-associative right_zeroed right_complementable unital distributive doubleLoopStr
for b₂ being FinSequence of the carrier of b₁ st ex b₃ being Nat st
( b₃ in dom b₂ & b₂ /. b₃ = 0. b₁ ) holds
Product b₂ = 0. b₁

proof end;

theorem Th7: :: POLYNOM2:7

for b₁ being non empty Abelian add-associative LoopStr
for b₂ being Element of b₁
for b₃, b₄ being FinSequence of the carrier of b₁ st len b₃ = len b₄ & ex b₅ being Nat st
( b₅ in dom b₃ & b₄ /. b₅ = b₂ + (b₃ /. b₅) & ( for b₆ being Nat st b₆ in dom b₃ & b₆ <> b₅ holds
b₄ /. b₆ = b₃ /. b₆ ) ) holds
Sum b₄ = b₂ + (Sum b₃)

proof end;

theorem Th8: :: POLYNOM2:8

for b₁ being non empty associative commutative doubleLoopStr
for b₂ being Element of b₁
for b₃, b₄ being FinSequence of the carrier of b₁ st len b₃ = len b₄ & ex b₅ being Nat st
( b₅ in dom b₃ & b₄ /. b₅ = b₂ * (b₃ /. b₅) & ( for b₆ being Nat st b₆ in dom b₃ & b₆ <> b₅ holds
b₄ /. b₆ = b₃ /. b₆ ) ) holds
Product b₄ = b₂ * (Product b₃)

proof end;

theorem Th9: :: POLYNOM2:9

for b₁ being set
for b₂ being empty Subset of b₁
for b₃ being Order of b₁ st b₃ linearly_orders b₂ holds
SgmX b₃,b₂ = {}

proof end;

theorem Th10: :: POLYNOM2:10

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Order of b₁ st b₃ linearly_orders b₂ holds
for b₄, b₅ being Nat st b₄ in dom (SgmX b₃,b₂) & b₅ in dom (SgmX b₃,b₂) & (SgmX b₃,b₂) /. b₄ = (SgmX b₃,b₂) /. b₅ holds
b₄ = b₅

proof end;

Lemma12: for b₁ being set
for b₂ being FinSequence of b₁ st dom b₂ <> {} holds
1 in dom b₂

proof end;

theorem Th11: :: POLYNOM2:11

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
for b₄ being finite Subset of b₁ st b₄ = {b₃} \/ b₂ holds
for b₅ being Order of b₁ st b₅ linearly_orders b₄ holds
for b₆ being Nat st b₆ in dom (SgmX b₅,b₄) & (SgmX b₅,b₄) /. b₆ = b₃ holds
for b₇ being Nat st 1 <= b₇ & b₇ <= b₆ - 1 holds
(SgmX b₅,b₄) /. b₇ = (SgmX b₅,b₂) /. b₇

proof end;

theorem Th12: :: POLYNOM2:12

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
for b₄ being finite Subset of b₁ st b₄ = {b₃} \/ b₂ holds
for b₅ being Order of b₁ st b₅ linearly_orders b₄ holds
for b₆ being Nat st b₆ in dom (SgmX b₅,b₄) & (SgmX b₅,b₄) /. b₆ = b₃ holds
for b₇ being Nat st b₆ <= b₇ & b₇ <= len (SgmX b₅,b₂) holds
(SgmX b₅,b₄) /. (b₇ + 1) = (SgmX b₅,b₂) /. b₇

proof end;

theorem Th13: :: POLYNOM2:13

for b₁ being non empty set
for b₂ being finite Subset of b₁
for b₃ being Element of b₁ st not b₃ in b₂ holds
for b₄ being finite Subset of b₁ st b₄ = {b₃} \/ b₂ holds
for b₅ being Order of b₁ st b₅ linearly_orders b₄ holds
for b₆ being Nat st b₆ + 1 in dom (SgmX b₅,b₄) & (SgmX b₅,b₄) /. (b₆ + 1) = b₃ holds
SgmX b₅,b₄ = Ins (SgmX b₅,b₂),b₆,b₃

proof end;

theorem Th14: :: POLYNOM2:14

for b₁ being set
for b₂ being bag of b₁ st support b₂ = {} holds
b₂ = EmptyBag b₁

proof end;

Lemma17: for b₁ being set
for b₂ being bag of b₁ holds b₂ is PartFunc of b₁, NAT

proof end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
attr a₂ is empty means :Def1: :: POLYNOM2:def 1
a₂ = EmptyBag a₁;

end;

:: deftheorem Def1 defines empty POLYNOM2:def 1 :

registration

let c₁ be non empty set ;
cluster non empty M28(a₁);
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
redefine func support as support c₂ -> finite Subset of a₁;
coherence

proof end;

end;

theorem Th15: :: POLYNOM2:15

for b₁ being Ordinal
for b₂ being bag of b₁ holds RelIncl b₁ linearly_orders support b₂

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be bag of c₁;
redefine func * as c₃ * c₂ -> PartFunc of NAT , NAT ;
coherence

proof end;

end;

definition

let c₁ be Ordinal;
let c₂ be bag of c₁;
let c₃ be non empty unital non trivial doubleLoopStr ;
let c₄ be Function of c₁,c₃;
func eval c₂,c₄ -> Element of a₃ means :Def2: :: POLYNOM2:def 2
ex b₁ being FinSequence of the carrier of a₃ st
( len b₁ = len (SgmX (RelIncl a₁),(support a₂)) & a₅ = Product b₁ & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
b₁ /. b₂ = (power a₃) . ((a₄ * (SgmX (RelIncl a₁),(support a₂))) /. b₂),((a₂ * (SgmX (RelIncl a₁),(support a₂))) /. b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines eval POLYNOM2:def 2 :

Lemma21: for b₁ being set holds support (EmptyBag b₁) = {}

proof end;

theorem Th16: :: POLYNOM2:16

for b₁ being Ordinal
for b₂ being non empty unital non trivial doubleLoopStr
for b₃ being Function of b₁,b₂ holds eval (EmptyBag b₁),b₃ = 1. b₂

proof end;

theorem Th17: :: POLYNOM2:17

for b₁ being Ordinal
for b₂ being non empty unital non trivial doubleLoopStr
for b₃ being set
for b₄ being bag of b₁ st support b₄ = {b₃} holds
for b₅ being Function of b₁,b₂ holds eval b₄,b₅ = (power b₂) . (b₅ . b₃),(b₄ . b₃)

proof end;

Lemma24: for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b₃, b₄ being bag of b₁
for b₅ being set st not b₅ in support b₃ & support b₄ = (support b₃) \/ {b₅} & ( for b₆ being set st b₆ <> b₅ holds
b₄ . b₆ = b₃ . b₆ ) holds
for b₆ being Function of b₁,b₂
for b₇ being Element of b₂ st b₇ = (power b₂) . (b₆ . b₅),(b₄ . b₅) holds
eval b₄,b₆ = b₇ * (eval b₃,b₆)

proof end;

Lemma25: for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b₃ being bag of b₁ st ex b₄ being set st support b₃ = {b₄} holds
for b₄ being bag of b₁
for b₅ being Function of b₁,b₂ holds eval (b₃ + b₄),b₅ = (eval b₃,b₅) * (eval b₄,b₅)

proof end;

theorem Th18: :: POLYNOM2:18

for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b₃, b₄ being bag of b₁
for b₅ being Function of b₁,b₂ holds eval (b₃ + b₄),b₅ = (eval b₃,b₅) * (eval b₄,b₅)

proof end;

registration

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₃, c₄ be Polynomial of c₁,c₂;
cluster a₃ - a₄ -> finite-Support ;
coherence

proof end;

end;

theorem Th19: :: POLYNOM2:19

for b₁ being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₂ being Ordinal
for b₃ being Polynomial of b₂,b₁ st Support b₃ = {} holds
b₃ = 0_ b₂,b₁

proof end;

registration

end;

theorem Th20: :: POLYNOM2:20

proof end;

definition

let c₁ be Ordinal;
let c₂ be Element of Bags c₁;
func c₂ @ -> bag of a₁ equals :: POLYNOM2:def 3
a₂;
correctness ;

end;

:: deftheorem Def3 defines @ POLYNOM2:def 3 :

definition

let c₁ be Ordinal;
let c₂ be non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr ;
let c₃ be Polynomial of c₁,c₂;
let c₄ be Function of c₁,c₂;
func eval c₃,c₄ -> Element of a₂ means :Def4: :: POLYNOM2:def 4
ex b₁ being FinSequence of the carrier of a₂ st
( len b₁ = len (SgmX (BagOrder a₁),(Support a₃)) & a₅ = Sum b₁ & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
b₁ /. b₂ = ((a₃ * (SgmX (BagOrder a₁),(Support a₃))) /. b₂) * (eval (((SgmX (BagOrder a₁),(Support a₃)) /. b₂) @ ),a₄) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines eval POLYNOM2:def 4 :

theorem Th21: :: POLYNOM2:21

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂
for b₄ being bag of b₁ st Support b₃ = {b₄} holds
for b₅ being Function of b₁,b₂ holds eval b₃,b₅ = (b₃ . b₄) * (eval b₄,b₅)

proof end;

theorem Th22: :: POLYNOM2:22

for b₁ being Ordinal
for b₂ being non empty add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Function of b₁,b₂ holds eval (0_ b₁,b₂),b₃ = 0. b₂

proof end;

theorem Th23: :: POLYNOM2:23

proof end;

theorem Th24: :: POLYNOM2:24

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

proof end;

Lemma34: for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂
for b₅ being Function of b₁,b₂
for b₆ being bag of b₁ st not b₆ in Support b₃ & Support b₄ = (Support b₃) \/ {b₆} & ( for b₇ being bag of b₁ st b₇ <> b₆ holds
b₄ . b₇ = b₃ . b₇ ) holds
eval b₄,b₅ = (eval b₃,b₅) + ((b₄ . b₆) * (eval b₆,b₅))

proof end;

Lemma35: for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂ st ex b₄ being bag of b₁ st Support b₃ = {b₄} holds
for b₄ being Polynomial of b₁,b₂
for b₅ being Function of b₁,b₂ holds eval (b₃ + b₄),b₅ = (eval b₃,b₅) + (eval b₄,b₅)

proof end;

theorem Th25: :: POLYNOM2:25

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

proof end;

theorem Th26: :: POLYNOM2:26

proof end;

Lemma37: for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b₃, b₄ being Polynomial of b₁,b₂
for b₅, b₆ being bag of b₁ st Support b₃ = {b₅} & Support b₄ = {b₆} holds
for b₇ being Function of b₁,b₂ holds eval (b₃ *' b₄),b₇ = (eval b₃,b₇) * (eval b₄,b₇)

proof end;

Lemma38: for b₁ being Ordinal
for b₂ being non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr
for b₃ being Polynomial of b₁,b₂ st ex b₄ being bag of b₁ st Support b₃ = {b₄} holds
for b₄ being Polynomial of b₁,b₂
for b₅ being Function of b₁,b₂ holds eval (b₄ *' b₃),b₅ = (eval b₄,b₅) * (eval b₃,b₅)

proof end;

theorem Th27: :: POLYNOM2:27

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

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Polynom-Evaluation POLYNOM2:def 5 :

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
cluster Polynom-Ring a₁,a₂ -> unital ;
coherence ;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative distributive non trivial doubleLoopStr ;
let c₃ be Function of c₁,c₂;
cluster Polynom-Evaluation a₁,a₂,a₃ -> unity-preserving ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
let c₃ be Function of c₁,c₂;
cluster Polynom-Evaluation a₁,a₂,a₃ -> additive unity-preserving multiplicative ;
coherence

proof end;

end;

registration

let c₁ be Ordinal;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non trivial doubleLoopStr ;
let c₃ be Function of c₁,c₂;
cluster Polynom-Evaluation a₁,a₂,a₃ -> RingHomomorphism additive unity-preserving multiplicative ;
coherence

proof end;

end;