let L be non empty right_complementable add-associative right_zeroed unital associative distributive doubleLoopStr ; :: thesis: 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))
let p, q be Polynomial of L; :: thesis: ( len p > 0 & len q > 0 implies 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)) )
assume A1: ( len p > 0 & len q > 0 ) ; :: thesis: 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))
let x be Element of L; :: thesis: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
set LMp = Leading-Monomial p;
set LMq = Leading-Monomial q;
consider F being FinSequence of the carrier of L such that
A2: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = Sum F and
A3: len F = len ((Leading-Monomial p) *' (Leading-Monomial q)) and
A4: for n being Element of NAT st n in dom F holds
F . n = (((Leading-Monomial p) *' (Leading-Monomial q)) . (n -' 1)) * ((power L) . x,(n -' 1)) by Def2;
A5: ( len p >= 0 + 1 & len q >= 0 + 1 ) by A1, NAT_1:13;
then A6: ( (len p) - 1 >= 0 & (len q) - 1 >= 0 ) by XREAL_1:21;
then A7: ( (len p) - 1 = (len p) -' 1 & (len q) - 1 = (len q) -' 1 ) by XREAL_0:def 2;
A8: (len p) + (len q) >= 0 + (1 + 1) by A5, XREAL_1:9;
then A9: ((len p) + (len q)) - 1 >= 1 by XREAL_1:21;
then reconsider i1 = ((len p) + (len q)) - 1 as Element of NAT by INT_1:16;
A10: (i1 -' 1) + 1 = i1 by A9, XREAL_1:237;
consider r being FinSequence of the carrier of L such that
A11: len r = (i1 -' 1) + 1 and
A12: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = Sum r and
A13: for k being Element of NAT st k in dom r holds
r . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' k)) by POLYNOM3:def 11;
((len p) + ((len q) - 1)) - (len p) >= 0 by A5, XREAL_1:21;
then A14: i1 -' (len p) = ((len p) + ((len q) - 1)) - (len p) by XREAL_0:def 2
.= (len q) -' 1 by A6, XREAL_0:def 2 ;
A15: ((len p) + (len q)) - 2 >= 0 by A8, XREAL_1:21;
((len p) + (len q)) - (1 + 1) >= 0 by A8, XREAL_1:21;
then A16: i1 -' 1 = (((len p) + (len q)) - 1) - 1 by XREAL_0:def 2
.= ((len p) + (len q)) -' 2 by A15, XREAL_0:def 2 ;
(len p) + 0 <= (len p) + ((len q) - 1) by A6, XREAL_1:9;
then len p in Seg (len r) by A5, A10, A11, FINSEQ_1:3;
then A17: len p in dom r by FINSEQ_1:def 3;
then A18: r . (len p) = ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A10, A13, A14;
now
let i be Element of NAT ; :: thesis: ( i in dom r & i <> len p implies r /. i = 0. L )
assume that
A19: i in dom r and
A20: i <> len p ; :: thesis: r /. i = 0. L
i in Seg (len r) by A19, FINSEQ_1:def 3;
then i >= 0 + 1 by FINSEQ_1:3;
then i - 1 >= 0 by XREAL_1:21;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A21: i -' 1 <> (len p) -' 1 by A7, A20;
thus r /. i = r . i by A19, PARTFUN1:def 8
.= ((Leading-Monomial p) . (i -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A13, A19
.= (0. L) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A21, Def1
.= 0. L by VECTSP_1:39 ; :: thesis: verum
end;
then A22: Sum r = r /. (len p) by A17, POLYNOM2:5
.= ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A17, A18, PARTFUN1:def 8
.= (p . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by Def1
.= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by Def1 ;
A23: now
let i be Element of NAT ; :: thesis: ( i in dom F & i <> i1 implies F /. i = 0. L )
assume that
A24: i in dom F and
A25: i <> i1 ; :: thesis: F /. i = 0. L
consider r1 being FinSequence of the carrier of L such that
A26: len r1 = (i -' 1) + 1 and
A27: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i -' 1) = Sum r1 and
A28: for k being Element of NAT st k in dom r1 holds
r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' k)) by POLYNOM3:def 11;
i in Seg (len F) by A24, FINSEQ_1:def 3;
then i >= 1 by FINSEQ_1:3;
then A29: (i -' 1) + 1 = i by XREAL_1:237;
A30: now
let j be Element of NAT ; :: thesis: ( j in dom r1 implies r1 . b1 = 0. L )
assume A31: j in dom r1 ; :: thesis: r1 . b1 = 0. L
then j in Seg (len r1) by FINSEQ_1:def 3;
then j >= 0 + 1 by FINSEQ_1:3;
then j - 1 >= 0 by XREAL_1:21;
then A32: j -' 1 = j - 1 by XREAL_0:def 2;
per cases ( j <> len p or j = len p ) ;
suppose j <> len p ; :: thesis: r1 . b1 = 0. L
then A33: j -' 1 <> (len p) -' 1 by A7, A32;
thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A28, A31
.= (0. L) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A33, Def1
.= 0. L by VECTSP_1:39 ; :: thesis: verum
end;
suppose A34: j = len p ; :: thesis: r1 . b1 = 0. L
j in Seg (len r1) by A31, FINSEQ_1:def 3;
then i >= 0 + j by A26, A29, FINSEQ_1:3;
then i - j >= 0 by XREAL_1:21;
then i -' (len p) = i - (len p) by A34, XREAL_0:def 2;
then A35: i -' (len p) <> (len q) -' 1 by A7, A25;
thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (i -' (len p))) by A28, A29, A31, A34
.= ((Leading-Monomial p) . (j -' 1)) * (0. L) by A35, Def1
.= 0. L by VECTSP_1:36 ; :: thesis: verum
end;
end;
end;
thus F /. i = F . i by A24, PARTFUN1:def 8
.= (Sum r1) * ((power L) . x,(i -' 1)) by A4, A24, A27
.= (0. L) * ((power L) . x,(i -' 1)) by A30, POLYNOM3:1
.= 0. L by VECTSP_1:39 ; :: thesis: verum
end;
per cases ( ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L or ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ) ;
suppose ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L ; :: thesis: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
then len F > i1 -' 1 by A3, ALGSEQ_1:22;
then len F >= i1 by A10, NAT_1:13;
then i1 in Seg (len F) by A9, FINSEQ_1:3;
then A36: i1 in dom F by FINSEQ_1:def 3;
hence eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = F /. i1 by A2, A23, POLYNOM2:5
.= F . i1 by A36, PARTFUN1:def 8
.= ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2)) by A4, A12, A16, A22, A36 ;
:: thesis: verum
end;
suppose A37: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L ; :: thesis: eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2))
now
let j be Nat; :: thesis: ( j >= 0 implies ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L )
assume j >= 0 ; :: thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L
j in NAT by ORDINAL1:def 13;
then consider r1 being FinSequence of the carrier of L such that
A38: len r1 = j + 1 and
A39: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = Sum r1 and
A40: for k being Element of NAT st k in dom r1 holds
r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by POLYNOM3:def 11;
now
per cases ( j = i1 -' 1 or j <> i1 -' 1 ) ;
suppose A41: j <> i1 -' 1 ; :: thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L
now
let k be Element of NAT ; :: thesis: ( k in dom r1 implies r1 . b1 = 0. L )
assume A42: k in dom r1 ; :: thesis: r1 . b1 = 0. L
per cases ( k -' 1 <> (len p) -' 1 or k -' 1 = (len p) -' 1 ) ;
suppose A43: k -' 1 <> (len p) -' 1 ; :: thesis: r1 . b1 = 0. L
thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A40, A42
.= (0. L) * ((Leading-Monomial q) . ((j + 1) -' k)) by A43, Def1
.= 0. L by VECTSP_1:39 ; :: thesis: verum
end;
suppose A44: k -' 1 = (len p) -' 1 ; :: thesis: r1 . b1 = 0. L
k in Seg (len r1) by A42, FINSEQ_1:def 3;
then A45: ( 0 + 1 <= k & 0 + k <= j + 1 ) by A38, FINSEQ_1:3;
then k - 1 >= 0 by XREAL_1:21;
then A46: k -' 1 = k - 1 by XREAL_0:def 2;
(j + 1) - k >= 0 by A45, XREAL_1:21;
then A47: (j + 1) -' k = (j - (len p)) + 1 by A7, A44, A46, XREAL_0:def 2;
A48: (j - (len p)) + 1 <> ((i1 -' 1) - (len p)) + 1 by A41;
thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A40, A42
.= ((Leading-Monomial p) . (k -' 1)) * (0. L) by A7, A10, A47, A48, Def1
.= 0. L by VECTSP_1:36 ; :: thesis: verum
end;
end;
end;
hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L by A39, POLYNOM3:1; :: thesis: verum
end;
end;
end;
hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L ; :: thesis: verum
end;
then A49: 0 is_at_least_length_of (Leading-Monomial p) *' (Leading-Monomial q) by ALGSEQ_1:def 3;
len ((Leading-Monomial p) *' (Leading-Monomial q)) = 0 by A49, ALGSEQ_1:def 4;
then (Leading-Monomial p) *' (Leading-Monomial q) = 0_. L by Th8;
then eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = 0. L by Th20;
hence eval ((Leading-Monomial p) *' (Leading-Monomial q)),x = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . x,(((len p) + (len q)) -' 2)) by A12, A22, A37, VECTSP_1:39; :: thesis: verum
end;
end;