:: POLYNOM3 semantic presentation

for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being FinSequence of the carrier of L st ( for i being Nat st i in dom p holds
p . i = 0. L ) holds
Sum p = 0. L

proof end;

theorem Th2: :: POLYNOM3:2

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

proof end;

theorem Th3: :: POLYNOM3:3

for p being FinSequence of REAL holds Sum p = Sum (Rev p)

proof end;

theorem Th4: :: POLYNOM3:4

for p being FinSequence of NAT
for i being Nat st i in dom p holds
Sum p >= p . i

proof end;

definition

let D be non empty set ;
let i be Nat;
let p be FinSequence of D;
:: original: Del
redefine func Del p,i -> FinSequence of D;
coherence by FINSEQ_3:114;

end;

definition

let D be non empty set ;
let a, b be Element of D;
:: original: <*
redefine func <*a,b*> -> Element of 2 -tuples_on D;
coherence by FINSEQ_2:121;

end;

definition

let D be non empty set ;
let k, n be Nat;
let p be Element of k -tuples_on D;
let q be Element of n -tuples_on D;
:: original: ^
redefine func p ^ q -> Element of (k + n) -tuples_on D;
coherence by FINSEQ_2:127;

end;

registration

let D be non empty set ;
let n be Nat;
cluster -> FinSequence-yielding FinSequence of n -tuples_on D;
coherence

proof end;

end;

definition

let D be non empty set ;
let k, n be Nat;
let p be FinSequence of k -tuples_on D;
let q be FinSequence of n -tuples_on D;
:: original: ^^
redefine func p ^^ q -> Element of ((k + n) -tuples_on D) * ;
coherence

proof end;

end;

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

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

proof end;

definition

let n be Nat;
let p, q be Element of n -tuples_on NAT ;
pred p < q means :Def1: :: POLYNOM3:def 1
ex i being Nat st
( i in Seg n & p . i < q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) );
asymmetry

proof end;

end;

:: deftheorem Def1 defines < POLYNOM3:def 1 :

notation

let n be Nat;
let p, q be Element of n -tuples_on NAT ;
synonym q > p for p < q;

end;

definition

let n be Nat;
let p, q be Element of n -tuples_on NAT ;
pred p <= q means :Def2: :: POLYNOM3:def 2
( p < q or p = q );
reflexivity ;

end;

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

notation

let n be Nat;
let p, q be Element of n -tuples_on NAT ;
synonym q >= p for p <= q;

end;

theorem Th5: :: POLYNOM3:5

for n being Nat
for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

proof end;

theorem Th6: :: POLYNOM3:6

for n being Nat
for p, q being Element of n -tuples_on NAT st p <> q holds
ex i being Nat st
( i in Seg n & p . i <> q . i & ( for k being Nat st 1 <= k & k < i holds
p . k = q . k ) )

proof end;

theorem Th7: :: POLYNOM3:7

for n being Nat
for p, q being Element of n -tuples_on NAT holds
( p <= q or p > q )

proof end;

definition

let n be Nat;
func TuplesOrder n -> Order of n -tuples_on NAT means :Def3: :: POLYNOM3:def 3
for p, q being Element of n -tuples_on NAT holds
( [p,q] in it iff p <= q );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines TuplesOrder POLYNOM3:def 3 :

registration

let n be Nat;
cluster TuplesOrder n -> being_linear-order ;
coherence

proof end;

end;

definition

let i be non empty Nat;
let n be Nat;
func Decomp n,i -> FinSequence of i -tuples_on NAT means :Def4: :: POLYNOM3:def 4
ex A being finite Subset of (i -tuples_on NAT ) st
( it = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :

registration

let i be non empty Nat;
let n be Nat;
cluster Decomp n,i -> non empty one-to-one FinSequence-yielding ;
coherence

proof end;

end;

theorem Th8: :: POLYNOM3:8

for n being Nat holds len (Decomp n,1) = 1

proof end;

theorem Th9: :: POLYNOM3:9

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

proof end;

theorem :: POLYNOM3:10

for n being Nat holds Decomp n,1 = <*<*n*>*>

proof end;

theorem Th11: :: POLYNOM3:11

for i, j, n, k1, k2 being Nat st (Decomp n,2) . i = <*k1,(n -' k1)*> & (Decomp n,2) . j = <*k2,(n -' k2)*> holds
( i < j iff k1 < k2 )

proof end;

theorem Th12: :: POLYNOM3:12

for i, n, k1, k2 being Nat st (Decomp n,2) . i = <*k1,(n -' k1)*> & (Decomp n,2) . (i + 1) = <*k2,(n -' k2)*> holds
k2 = k1 + 1

proof end;

theorem Th13: :: POLYNOM3:13

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

proof end;

theorem Th14: :: POLYNOM3:14

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

proof end;

definition

let L be non empty HGrStr ;
let p, q, r be sequence of L;
let t be FinSequence of 3 -tuples_on NAT ;
func prodTuples p,q,r,t -> Element of the carrier of L * means :Def5: :: POLYNOM3:def 5
( len it = len t & ( for k being Nat st k in dom t holds
it . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines prodTuples POLYNOM3:def 5 :

theorem Th15: :: POLYNOM3:15

for L being non empty HGrStr
for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of dom t
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples p,q,r,t1 = (prodTuples p,q,r,t) * P

proof end;

theorem Th16: :: POLYNOM3:16

for D being set
for f being FinSequence of D *
for i being Nat holds Card (f | i) = (Card f) | i

proof end;

theorem Th17: :: POLYNOM3:17

for p being FinSequence of REAL
for q being FinSequence of NAT st p = q holds
for i being Nat holds p | i = q | i

proof end;

theorem Th18: :: POLYNOM3:18

for p being FinSequence of NAT
for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)

proof end;

theorem Th19: :: POLYNOM3:19

for D being set
for p being FinSequence of D
for i being Nat st i < len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>

proof end;

theorem Th20: :: POLYNOM3:20

for p being FinSequence of REAL
for i being Nat st i < len p holds
Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1))

proof end;

theorem Th21: :: POLYNOM3:21

for p being FinSequence of NAT
for i, j, k1, k2 being Nat st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )

proof end;

theorem Th22: :: POLYNOM3:22

for D1, D2 being set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Nat st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )

proof end;

definition

let L be non empty ZeroStr ;
mode Polynomial of L is AlgSequence of L;

end;

theorem Th23: :: POLYNOM3:23

for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat holds
( n >= len p iff n is_at_least_length_of p )

proof end;

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

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

proof end;

definition

let L be non empty LoopStr ;
let p, q be sequence of L;
func p + q -> sequence of L means :Def6: :: POLYNOM3:def 6
for n being Nat holds it . n = (p . n) + (q . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + POLYNOM3:def 6 :

registration

let L be non empty right_zeroed LoopStr ;
let p, q be Polynomial of L;
cluster p + q -> finite-Support ;
coherence

proof end;

end;

theorem Th24: :: POLYNOM3:24

for L being non empty right_zeroed LoopStr
for p, q being Polynomial of L
for n being Nat st n is_at_least_length_of p & n is_at_least_length_of q holds
n is_at_least_length_of p + q

proof end;

theorem :: POLYNOM3:25

for L being non empty right_zeroed LoopStr
for p, q being Polynomial of L holds support (p + q) c= (support p) \/ (support q)

proof end;

definition

let L be non empty Abelian LoopStr ;
let p, q be sequence of L;
:: original: +
redefine func p + q -> sequence of L;
commutativity

proof end;

end;

theorem Th26: :: POLYNOM3:26

for L being non empty add-associative LoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)

proof end;

definition

let L be non empty LoopStr ;
let p be sequence of L;
func - p -> sequence of L means :Def7: :: POLYNOM3:def 7
for n being Nat holds it . n = - (p . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - POLYNOM3:def 7 :

registration

let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p be Polynomial of L;
cluster - p -> finite-Support ;
coherence

proof end;

end;

definition

let L be non empty LoopStr ;
let p, q be sequence of L;
func p - q -> sequence of L equals :: POLYNOM3:def 8
p + (- q);
coherence ;

end;

:: deftheorem defines - POLYNOM3:def 8 :

registration

let L be non empty add-associative right_zeroed right_complementable LoopStr ;
let p, q be Polynomial of L;
cluster p - q -> finite-Support ;
coherence ;

end;

theorem Th27: :: POLYNOM3:27

for L being non empty LoopStr
for p, q being sequence of L
for n being Nat holds (p - q) . n = (p . n) - (q . n)

proof end;

definition

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

end;

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

registration

let L be non empty ZeroStr ;
cluster 0_. L -> finite-Support ;
coherence

proof end;

end;

theorem Th28: :: POLYNOM3:28

for L being non empty ZeroStr
for n being Nat holds (0_. L) . n = 0. L by FUNCOP_1:13;

theorem Th29: :: POLYNOM3:29

for L being non empty right_zeroed LoopStr
for p being sequence of L holds p + (0_. L) = p

proof end;

theorem Th30: :: POLYNOM3:30

for L being non empty add-associative right_zeroed right_complementable LoopStr
for p being sequence of L holds p - p = 0_. L

proof end;

definition

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

end;

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

registration

let L be non empty multLoopStr_0 ;
cluster 1_. L -> finite-Support ;
coherence

proof end;

end;

theorem Th31: :: POLYNOM3:31

for L being non empty multLoopStr_0 holds
( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )

proof end;

definition

let L be non empty doubleLoopStr ;
let p, q be sequence of L;
func p *' q -> sequence of L means :Def11: :: POLYNOM3:def 11
for i being Nat ex r being FinSequence of the carrier of L st
( len r = i + 1 & it . i = Sum r & ( for k being Nat st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
let p, q be Polynomial of L;
cluster p *' q -> finite-Support ;
coherence

proof end;

end;

theorem Th32: :: POLYNOM3:32

for L being non empty Abelian add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p, q, r being sequence of L holds p *' (q + r) = (p *' q) + (p *' r)

proof end;

theorem Th33: :: POLYNOM3:33

for L being non empty Abelian add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for p, q, r being sequence of L holds (p + q) *' r = (p *' r) + (q *' r)

proof end;

theorem Th34: :: POLYNOM3:34

for L being non empty Abelian add-associative right_zeroed right_complementable unital associative distributive doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)

proof end;

definition

let L be non empty Abelian add-associative right_zeroed commutative doubleLoopStr ;
let p, q be sequence of L;
:: original: *'
redefine func p *' q -> sequence of L;
commutativity

proof end;

end;

theorem :: POLYNOM3:35

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

proof end;

theorem Th36: :: POLYNOM3:36

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

proof end;

definition

let L be non empty add-associative right_zeroed right_complementable distributive doubleLoopStr ;
func Polynom-Ring L -> non empty strict doubleLoopStr means :Def12: :: POLYNOM3:def 12
( ( for x being set holds
( x in the carrier of it iff x is Polynomial of L ) ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of it
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & 0. it = 0_. L & 1_ it = 1_. L );
existence

proof end;