:: POLYNOM3 semantic presentation

theorem Th1: :: POLYNOM3:1

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of the carrier of b₁ st ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = 0. b₁ ) holds
Sum b₂ = 0. b₁

proof end;

theorem Th2: :: POLYNOM3:2

for b₁ being non empty Abelian add-associative right_zeroed LoopStr
for b₂ being FinSequence of the carrier of b₁ holds Sum b₂ = Sum (Rev b₂)

proof end;

theorem Th3: :: POLYNOM3:3

for b₁ being FinSequence of REAL holds Sum b₁ = Sum (Rev b₁)

proof end;

theorem Th4: :: POLYNOM3:4

for b₁ being FinSequence of NAT
for b₂ being Nat st b₂ in dom b₁ holds
Sum b₁ >= b₁ . b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be FinSequence of c₁;
redefine func Del as Del c₃,c₂ -> FinSequence of a₁;
coherence by FINSEQ_3:114;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of c₁;
redefine func <* as <*c₂,c₃*> -> Element of 2 -tuples_on a₁;
coherence by FINSEQ_2:121;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Nat;
let c₄ be Element of c₂ -tuples_on c₁;
let c₅ be Element of c₃ -tuples_on c₁;
redefine func ^ as c₄ ^ c₅ -> Element of (a₂ + a₃) -tuples_on a₁;
coherence by FINSEQ_2:127;

end;

registration

let c₁ be non empty set ;
let c₂ be Nat;
cluster -> FinSequence-yielding FinSequence of a₂ -tuples_on a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Nat;
let c₄ be FinSequence of c₂ -tuples_on c₁;
let c₅ be FinSequence of c₃ -tuples_on c₁;
redefine func ^^ as c₄ ^^ c₅ -> Element of ((a₂ + a₃) -tuples_on a₁) * ;
coherence

proof end;

end;

scheme :: POLYNOM3:sch 1
s1{ F₁() -> non empty set , F₂() -> Nat, F₃( Nat) -> Nat, F₄( set , set ) -> Element of F₁() } :

ex b₁ being FinSequence of F₁() * st
( len b₁ = F₂() & ( for b₂ being Nat st b₂ in Seg F₂() holds
( len (b₁ /. b₂) = F₃(b₂) & ( for b₃ being Nat st b₃ in dom (b₁ /. b₂) holds
(b₁ /. b₂) . b₃ = F₄(b₂,b₃) ) ) ) )

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on NAT ;
pred c₂ < c₃ means :Def1: :: POLYNOM3:def 1
ex b₁ being Nat st
( b₁ in Seg a₁ & a₂ . b₁ < a₃ . b₁ & ( for b₂ being Nat st 1 <= b₂ & b₂ < b₁ holds
a₂ . b₂ = a₃ . b₂ ) );
asymmetry

proof end;

end;

:: deftheorem Def1 defines < POLYNOM3:def 1 :

notation

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on NAT ;
synonym c₃ > c₂ for c₂ < c₃;

end;

definition

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on NAT ;
pred c₂ <= c₃ means :Def2: :: POLYNOM3:def 2
( a₂ < a₃ or a₂ = a₃ );
reflexivity ;

end;

:: deftheorem Def2 defines <= POLYNOM3:def 2 :

notation

let c₁ be Nat;
let c₂, c₃ be Element of c₁ -tuples_on NAT ;
synonym c₃ >= c₂ for c₂ <= c₃;

end;

theorem Th5: :: POLYNOM3:5

for b₁ being Nat
for b₂, b₃, b₄ being Element of b₁ -tuples_on NAT holds
( ( b₂ < b₃ & b₃ < b₄ implies b₂ < b₄ ) & ( ( ( b₂ < b₃ & b₃ <= b₄ ) or ( b₂ <= b₃ & b₃ < b₄ ) or ( b₂ <= b₃ & b₃ <= b₄ ) ) implies b₂ <= b₄ ) )

proof end;

theorem Th6: :: POLYNOM3:6

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on NAT st b₂ <> b₃ holds
ex b₄ being Nat st
( b₄ in Seg b₁ & b₂ . b₄ <> b₃ . b₄ & ( for b₅ being Nat st 1 <= b₅ & b₅ < b₄ holds
b₂ . b₅ = b₃ . b₅ ) )

proof end;

theorem Th7: :: POLYNOM3:7

for b₁ being Nat
for b₂, b₃ being Element of b₁ -tuples_on NAT holds
( b₂ <= b₃ or b₂ > b₃ )

proof end;

definition

let c₁ be Nat;
func TuplesOrder c₁ -> Order of a₁ -tuples_on NAT means :Def3: :: POLYNOM3:def 3
for b₁, b₂ being Element of a₁ -tuples_on NAT holds
( [b₁,b₂] in a₂ iff b₁ <= b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :

registration

let c₁ be Nat;
cluster TuplesOrder a₁ -> being_linear-order ;
coherence

proof end;

end;

definition

let c₁ be non empty Nat;
let c₂ be Nat;
func Decomp c₂,c₁ -> FinSequence of a₁ -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex b₁ being finite Subset of (a₁ -tuples_on NAT ) st
( a₃ = SgmX (TuplesOrder a₁),b₁ & ( for b₂ being Element of a₁ -tuples_on NAT holds
( b₂ in b₁ iff Sum b₂ = a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :

registration

let c₁ be non empty Nat;
let c₂ be Nat;
cluster Decomp a₂,a₁ -> non empty one-to-one FinSequence-yielding ;
coherence

proof end;

end;

theorem Th8: :: POLYNOM3:8

for b₁ being Nat holds len (Decomp b₁,1) = 1

proof end;

theorem Th9: :: POLYNOM3:9

for b₁ being Nat holds len (Decomp b₁,2) = b₁ + 1

proof end;

theorem Th10: :: POLYNOM3:10

for b₁ being Nat holds Decomp b₁,1 = <*<*b₁*>*>

proof end;

theorem Th11: :: POLYNOM3:11

for b₁, b₂, b₃, b₄, b₅ being Nat st (Decomp b₃,2) . b₁ = <*b₄,(b₃ -' b₄)*> & (Decomp b₃,2) . b₂ = <*b₅,(b₃ -' b₅)*> holds
( b₁ < b₂ iff b₄ < b₅ )

proof end;

theorem Th12: :: POLYNOM3:12

for b₁, b₂, b₃, b₄ being Nat st (Decomp b₂,2) . b₁ = <*b₃,(b₂ -' b₃)*> & (Decomp b₂,2) . (b₁ + 1) = <*b₄,(b₂ -' b₄)*> holds
b₄ = b₃ + 1

proof end;

theorem Th13: :: POLYNOM3:13

for b₁ being Nat holds (Decomp b₁,2) . 1 = <*0,b₁*>

proof end;

theorem Th14: :: POLYNOM3:14

for b₁, b₂ being Nat st b₂ in Seg (b₁ + 1) holds
(Decomp b₁,2) . b₂ = <*(b₂ -' 1),((b₁ + 1) -' b₂)*>

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃, c₄ be sequence of c₁;
let c₅ be FinSequence of 3 -tuples_on NAT ;
func prodTuples c₂,c₃,c₄,c₅ -> Element of the carrier of a₁ * means :Def5: :: POLYNOM3:def 5
( len a₆ = len a₅ & ( for b₁ being Nat st b₁ in dom a₅ holds
a₆ . b₁ = ((a₂ . ((a₅ /. b₁) /. 1)) * (a₃ . ((a₅ /. b₁) /. 2))) * (a₄ . ((a₅ /. b₁) /. 3)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :

theorem Th15: :: POLYNOM3:15

for b₁ being non empty HGrStr
for b₂, b₃, b₄ being sequence of b₁
for b₅ being FinSequence of 3 -tuples_on NAT
for b₆ being Permutation of dom b₅
for b₇ being FinSequence of 3 -tuples_on NAT st b₇ = b₅ * b₆ holds
prodTuples b₂,b₃,b₄,b₇ = (prodTuples b₂,b₃,b₄,b₅) * b₆

proof end;

theorem Th16: :: POLYNOM3:16

for b₁ being set
for b₂ being FinSequence of b₁ *
for b₃ being Nat holds Card (b₂ | b₃) = (Card b₂) | b₃

proof end;

theorem Th17: :: POLYNOM3:17

for b₁ being FinSequence of REAL
for b₂ being FinSequence of NAT st b₁ = b₂ holds
for b₃ being Nat holds b₁ | b₃ = b₂ | b₃

proof end;

theorem Th18: :: POLYNOM3:18

for b₁ being FinSequence of NAT
for b₂, b₃ being Nat st b₂ <= b₃ holds
Sum (b₁ | b₂) <= Sum (b₁ | b₃)

proof end;

theorem Th19: :: POLYNOM3:19

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Nat st b₃ < len b₂ holds
b₂ | (b₃ + 1) = (b₂ | b₃) ^ <*(b₂ . (b₃ + 1))*>

proof end;

theorem Th20: :: POLYNOM3:20

for b₁ being FinSequence of REAL
for b₂ being Nat st b₂ < len b₁ holds
Sum (b₁ | (b₂ + 1)) = (Sum (b₁ | b₂)) + (b₁ . (b₂ + 1))

proof end;

theorem Th21: :: POLYNOM3:21

for b₁ being FinSequence of NAT
for b₂, b₃, b₄, b₅ being Nat st b₂ < len b₁ & b₃ < len b₁ & 1 <= b₄ & 1 <= b₅ & b₄ <= b₁ . (b₂ + 1) & b₅ <= b₁ . (b₃ + 1) & (Sum (b₁ | b₂)) + b₄ = (Sum (b₁ | b₃)) + b₅ holds
( b₂ = b₃ & b₄ = b₅ )

proof end;

theorem Th22: :: POLYNOM3:22

for b₁, b₂ being set
for b₃ being FinSequence of b₁ *
for b₄ being FinSequence of b₂ *
for b₅, b₆, b₇, b₈ being Nat st b₅ in dom b₃ & b₆ in dom b₄ & b₇ in dom (b₃ . b₅) & b₈ in dom (b₄ . b₆) & Card b₃ = Card b₄ & (Sum ((Card b₃) | (b₅ -' 1))) + b₇ = (Sum ((Card b₄) | (b₆ -' 1))) + b₈ holds
( b₅ = b₆ & b₇ = b₈ )

proof end;

definition

let c₁ be non empty ZeroStr ;
mode Polynomial of a₁ is AlgSequence of a₁;

end;

theorem Th23: :: POLYNOM3:23

for b₁ being non empty ZeroStr
for b₂ being Polynomial of b₁
for b₃ being Nat holds
( b₃ >= len b₂ iff b₃ is_at_least_length_of b₂ )

proof end;

scheme :: POLYNOM3:sch 2
s2{ F₁() -> non empty LoopStr , F₂() -> Nat, F₃( Nat) -> Element of F₁() } :

ex b₁ being Polynomial of F₁() st
( len b₁ <= F₂() & ( for b₂ being Nat st b₂ < F₂() holds
b₁ . b₂ = F₃(b₂) ) )

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be sequence of c₁;
func c₂ + c₃ -> sequence of a₁ means :Def6: :: POLYNOM3:def 6
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + POLYNOM3:def 6 :

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂, c₃ be Polynomial of c₁;
cluster a₂ + a₃ -> finite-Support ;
coherence

proof end;

end;

theorem Th24: :: POLYNOM3:24

for b₁ being non empty right_zeroed LoopStr
for b₂, b₃ being Polynomial of b₁
for b₄ being Nat st b₄ is_at_least_length_of b₂ & b₄ is_at_least_length_of b₃ holds
b₄ is_at_least_length_of b₂ + b₃

proof end;

theorem Th25: :: POLYNOM3:25

for b₁ being non empty right_zeroed LoopStr
for b₂, b₃ being Polynomial of b₁ holds support (b₂ + b₃) c= (support b₂) \/ (support b₃)

proof end;

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be sequence of c₁;
redefine func + as c₂ + c₃ -> sequence of a₁;
commutativity

proof end;

end;

theorem Th26: :: POLYNOM3:26

for b₁ being non empty add-associative LoopStr
for b₂, b₃, b₄ being sequence of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂ be sequence of c₁;
func - c₂ -> sequence of a₁ means :Def7: :: POLYNOM3:def 7
for b₁ being Nat holds a₃ . b₁ = - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - POLYNOM3:def 7 :

registration

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

proof end;

end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be sequence of c₁;
func c₂ - c₃ -> sequence of a₁ equals :: POLYNOM3:def 8
a₂ + (- a₃);
coherence ;

end;

:: deftheorem Def8 defines - POLYNOM3:def 8 :

registration

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

end;

theorem Th27: :: POLYNOM3:27

for b₁ being non empty LoopStr
for b₂, b₃ being sequence of b₁
for b₄ being Nat holds (b₂ - b₃) . b₄ = (b₂ . b₄) - (b₃ . b₄)

proof end;

definition

let c₁ be non empty ZeroStr ;
func 0_. c₁ -> sequence of a₁ equals :: POLYNOM3:def 9
NAT --> (0. a₁);
coherence ;

end;

:: deftheorem Def9 defines 0_. POLYNOM3:def 9 :

registration

let c₁ be non empty ZeroStr ;
cluster 0_. a₁ -> finite-Support ;
coherence

proof end;

end;

theorem Th28: :: POLYNOM3:28

for b₁ being non empty ZeroStr
for b₂ being Nat holds (0_. b₁) . b₂ = 0. b₁ by FUNCOP_1:13;

theorem Th29: :: POLYNOM3:29

for b₁ being non empty right_zeroed LoopStr
for b₂ being sequence of b₁ holds b₂ + (0_. b₁) = b₂

proof end;

theorem Th30: :: POLYNOM3:30

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being sequence of b₁ holds b₂ - b₂ = 0_. b₁

proof end;

definition

let c₁ be non empty multLoopStr_0 ;
func 1_. c₁ -> sequence of a₁ equals :: POLYNOM3:def 10
(0_. a₁) +* 0,(1. a₁);
coherence ;

end;

:: deftheorem Def10 defines 1_. POLYNOM3:def 10 :

registration

let c₁ be non empty multLoopStr_0 ;
cluster 1_. a₁ -> finite-Support ;
coherence

proof end;

end;

theorem Th31: :: POLYNOM3:31

for b₁ being non empty multLoopStr_0 holds
( (1_. b₁) . 0 = 1. b₁ & ( for b₂ being Nat st b₂ <> 0 holds
(1_. b₁) . b₂ = 0. b₁ ) )

proof end;

definition

let c₁ be non empty doubleLoopStr ;
let c₂, c₃ be sequence of c₁;
func c₂ *' c₃ -> sequence of a₁ means :Def11: :: POLYNOM3:def 11
for b₁ being Nat ex b₂ being FinSequence of the carrier of a₁ st
( len b₂ = b₁ + 1 & a₄ . b₁ = Sum b₂ & ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = (a₂ . (b₃ -' 1)) * (a₃ . ((b₁ + 1) -' b₃)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines *' POLYNOM3:def 11 :

registration

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let c₂, c₃ be Polynomial of c₁;
cluster a₂ *' a₃ -> finite-Support ;
coherence

proof end;

end;

theorem Th32: :: POLYNOM3:32

for b₁ being non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃, b₄ being sequence of b₁ holds b₂ *' (b₃ + b₄) = (b₂ *' b₃) + (b₂ *' b₄)

proof end;

theorem Th33: :: POLYNOM3:33

for b₁ being non empty Abelian add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃, b₄ being sequence of b₁ holds (b₂ + b₃) *' b₄ = (b₂ *' b₄) + (b₃ *' b₄)

proof end;

theorem Th34: :: POLYNOM3:34

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

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
let c₂, c₃ be sequence of c₁;
redefine func *' as c₂ *' c₃ -> sequence of a₁;
commutativity

proof end;

end;

theorem Th35: :: POLYNOM3:35

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

proof end;

theorem Th36: :: POLYNOM3:36

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

proof end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
func Polynom-Ring c₁ -> non empty strict doubleLoopStr means :Def12: :: POLYNOM3:def 12
( ( for b₁ being set holds
( b₁ in the carrier of a₂ iff b₁ is Polynomial of a₁ ) ) & ( for b₁, b₂ being Element of a₂
for b₃, b₄ being sequence of a₁ st b₁ = b₃ & b₂ = b₄ holds
b₁ + b₂ = b₃ + b₄ ) & ( for b₁, b₂ being Element of a₂
for b₃, b₄ being sequence of a₁ st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ *' b₄ ) & 0. a₂ = 0_. a₁ & 1_ a₂ = 1_. a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Polynom-Ring POLYNOM3:def 12 :

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring a₁ -> non empty Abelian strict ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring a₁ -> non empty add-associative strict ;
coherence

proof end;

cluster Polynom-Ring a₁ -> non empty right_zeroed strict ;
coherence

proof end;

cluster Polynom-Ring a₁ -> non empty right_complementable strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable commutative distributive doubleLoopStr ;
cluster Polynom-Ring a₁ -> non empty Abelian add-associative right_zeroed right_complementable commutative strict ;
coherence

proof end;

end;

registration

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

proof end;

end;

E43: now

let c₁ be non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr ;
set c₂ = Polynom-Ring c₁;
let c₃, c₄ be Element of (Polynom-Ring c₁);
assume E44: c₄ = 1_ (Polynom-Ring c₁) ;
reconsider c₅ = c₃ as Polynomial of c₁ by Def12;
E45: 1_ (Polynom-Ring c₁) = 1_. c₁ by Def12;
hence c₃ * c₄ = c₅ *' (1_. c₁) by E44, Def12
.= c₃ by Th36 ;

reconsider c₆ = c₃, c₇ = c₄ as sequence of c₁ by Def12;
thus c₄ * c₃ = c₇ *' c₆ by Def12
.= c₅ *' (1_. c₁) by E45, E44
.= c₃ by Th36 ;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr ;
cluster Polynom-Ring a₁ -> non empty Abelian add-associative right_zeroed right_complementable unital commutative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr ;
cluster Polynom-Ring a₁ -> non empty Abelian add-associative right_zeroed right_complementable strict distributive ;
coherence

proof end;

end;

theorem Th37: :: POLYNOM3:37

for b₁ being non empty Abelian add-associative right_zeroed right_complementable commutative right_unital distributive doubleLoopStr holds 1. (Polynom-Ring b₁) = 1_. b₁

proof end;