let A, B be Ring; :: thesis: for p, q being Polynomial of A st A is Subring of B & len p > 0 & len q > 0 holds
for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))
let p, q be Polynomial of A; :: thesis: ( A is Subring of B & len p > 0 & len q > 0 implies for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2))) )
assume that
A0: A is Subring of B and
A1: len p > 0 and
A2: len q > 0 ; :: thesis: for x being Element of B holds Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))
A3: len q >= 0 + 1 by A2, NAT_1:13;
A5: len p >= 0 + 1 by A1, NAT_1:13;
A6: (len p) - 1 = (len p) -' 1 by A1, XREAL_0:def 2;
A7: (len p) + (len q) >= 0 + (1 + 1) by A5, A3, XREAL_1:7;
reconsider i1 = ((len p) + (len q)) - 1 as Element of NAT by A1, INT_1:3;
A9: (i1 -' 1) + 1 = i1 by A7, XREAL_1:19, XREAL_1:235;
set LMp = Leading-Monomial p;
set LMq = Leading-Monomial q;
let x be Element of B; :: thesis: Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))
consider F being FinSequence of B such that
A10: Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = Sum F and
A11: len F = len ((Leading-Monomial p) *' (Leading-Monomial q)) and
A12: for n being Element of NAT st n in dom F holds
F . n = (In ((((Leading-Monomial p) *' (Leading-Monomial q)) . (n -' 1)),B)) * ((power B) . (x,(n -' 1))) by Def1;
consider r being FinSequence of A such that
A13: len r = (i1 -' 1) + 1 and
A14: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = Sum r and
A15: 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 9;
(len p) + 0 <= (len p) + ((len q) - 1) by A2, XREAL_1:7;
then len p in Seg (len r) by A5, A9, A13;
then A16: len p in dom r by FINSEQ_1:def 3;
i1 -' (len p) = ((len p) + ((len q) - 1)) - (len p) by A2, XREAL_0:def 2
.= (len q) -' 1 by A2, XREAL_0:def 2 ;
then A17: r . (len p) = ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A9, A15, A16;
now :: thesis: for i being Element of NAT st i in dom r & i <> len p holds
r /. i = 0. A
let i be Element of NAT ; :: thesis: ( i in dom r & i <> len p implies r /. i = 0. A )
assume that
A18: i in dom r and
A19: i <> len p ; :: thesis: r /. i = 0. A
i >= 0 + 1 by A18, FINSEQ_3:25;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A20: i -' 1 <> (len p) -' 1 by A6, A19;
thus r /. i = r . i by A18, PARTFUN1:def 6
.= ((Leading-Monomial p) . (i -' 1)) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A15, A18
.= (0. A) * ((Leading-Monomial q) . (((i1 -' 1) + 1) -' i)) by A20, POLYNOM4:def 1
.= 0. A ; :: thesis: verum
end;
then A21: Sum r = r /. (len p) by A16, POLYNOM2:3
.= ((Leading-Monomial p) . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by A16, A17, PARTFUN1:def 6
.= (p . ((len p) -' 1)) * ((Leading-Monomial q) . ((len q) -' 1)) by POLYNOM4:def 1
.= (p . ((len p) -' 1)) * (q . ((len q) -' 1)) by POLYNOM4:def 1 ;
A22: (len q) - 1 = (len q) -' 1 by A2, XREAL_0:def 2;
A23: now :: thesis: for i being Element of NAT st i in dom F & i <> i1 holds
F /. i = 0. B
let i be Element of NAT ; :: thesis: ( i in dom F & i <> i1 implies F /. i = 0. B )
assume that
A24: i in dom F and
A25: i <> i1 ; :: thesis: F /. i = 0. B
consider r1 being FinSequence of A 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 9;
A29: (i -' 1) + 1 = i by A24, FINSEQ_3:25, XREAL_1:235;
A30: now :: thesis: for j being Element of NAT st j in dom r1 holds
r1 . j = 0. A
let j be Element of NAT ; :: thesis: ( j in dom r1 implies r1 . b1 = 0. A )
assume A31: j in dom r1 ; :: thesis: r1 . b1 = 0. A
then j >= 0 + 1 by FINSEQ_3:25;
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. A
then A33: j -' 1 <> (len p) -' 1 by A6, A32;
thus r1 . j = ((Leading-Monomial p) . (j -' 1)) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A28, A31
.= (0. A) * ((Leading-Monomial q) . (((i -' 1) + 1) -' j)) by A33, POLYNOM4:def 1
.= 0. A ; :: thesis: verum
end;
suppose A34: j = len p ; :: thesis: r1 . b1 = 0. A
j in Seg (len r1) by A31, FINSEQ_1:def 3;
then i >= 0 + j by A26, A29, FINSEQ_1:1;
then i -' (len p) = i - (len p) by A34, XREAL_1:19, XREAL_0:def 2;
then A35: i -' (len p) <> (len q) -' 1 by A22, 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. A) by A35, POLYNOM4:def 1
.= 0. A ; :: thesis: verum
end;
end;
end;
thus F /. i = F . i by A24, PARTFUN1:def 6
.= (In ((Sum r1),B)) * ((power B) . (x,(i -' 1))) by A12, A24, A27
.= (In ((0. A),B)) * ((power B) . (x,(i -' 1))) by A30, POLYNOM3:1
.= (0. B) * ((power B) . (x,(i -' 1))) by A0, Lm5
.= 0. B ; :: thesis: verum
end;
A36: ((len p) + (len q)) - 2 >= 0 by A7, XREAL_1:19;
((len p) + (len q)) - (1 + 1) >= 0 by A7, XREAL_1:19;
then A37: i1 -' 1 = (((len p) + (len q)) - 1) - 1 by XREAL_0:def 2
.= ((len p) + (len q)) -' 2 by A36, XREAL_0:def 2 ;
per cases ( ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. A or ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. A ) ;
suppose ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. A ; :: thesis: Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))
then len F >= i1 by A11, ALGSEQ_1:8, A9, NAT_1:13;
then A38: i1 in dom F by A7, XREAL_1:19, FINSEQ_3:25;
hence Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = F /. i1 by A10, A23, POLYNOM2:3
.= F . i1 by A38, PARTFUN1:def 6
.= (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2))) by A12, A14, A37, A21, A38 ;
:: thesis: verum
end;
suppose A39: ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. A ; :: thesis: Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2)))
now :: thesis: for j being Nat st j >= 0 holds
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A
let j be Nat; :: thesis: ( j >= 0 implies ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A )
assume j >= 0 ; :: thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A
j in NAT by ORDINAL1:def 12;
then consider r1 being FinSequence of A such that
A40: len r1 = j + 1 and
A41: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = Sum r1 and
A42: 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 9;
now :: thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A
per cases ( j = i1 -' 1 or j <> i1 -' 1 ) ;
suppose A43: j <> i1 -' 1 ; :: thesis: ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A
now :: thesis: for k being Element of NAT st k in dom r1 holds
r1 . k = 0. A
let k be Element of NAT ; :: thesis: ( k in dom r1 implies r1 . b1 = 0. A )
assume A44: k in dom r1 ; :: thesis: r1 . b1 = 0. A
per cases ( k -' 1 <> (len p) -' 1 or k -' 1 = (len p) -' 1 ) ;
suppose A45: k -' 1 <> (len p) -' 1 ; :: thesis: r1 . b1 = 0. A
thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44
.= (0. A) * ((Leading-Monomial q) . ((j + 1) -' k)) by A45, POLYNOM4:def 1
.= 0. A ; :: thesis: verum
end;
suppose A46: k -' 1 = (len p) -' 1 ; :: thesis: r1 . b1 = 0. A
A47: k in Seg (len r1) by A44, FINSEQ_1:def 3;
0 + 1 <= k by A44, FINSEQ_3:25;
then A48: k -' 1 = k - 1 by XREAL_0:def 2;
0 + k <= j + 1 by A40, A47, FINSEQ_1:1;
then (j + 1) - k >= 0 by XREAL_1:19;
then A49: (j + 1) -' k = (j - (len p)) + 1 by A6, A46, A48, XREAL_0:def 2;
A50: (j - (len p)) + 1 <> ((i1 -' 1) - (len p)) + 1 by A43;
thus r1 . k = ((Leading-Monomial p) . (k -' 1)) * ((Leading-Monomial q) . ((j + 1) -' k)) by A42, A44
.= ((Leading-Monomial p) . (k -' 1)) * (0. A) by A22, A9, A49, A50, POLYNOM4:def 1
.= 0. A ; :: thesis: verum
end;
end;
end;
hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A by A41, POLYNOM3:1; :: thesis: verum
end;
end;
end;
hence ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. A ; :: thesis: verum
end;
then 0 is_at_least_length_of (Leading-Monomial p) *' (Leading-Monomial q) ;
then len ((Leading-Monomial p) *' (Leading-Monomial q)) = 0 by ALGSEQ_1:def 3;
then A52: (Leading-Monomial p) *' (Leading-Monomial q) = 0_. A by POLYNOM4:5;
0. B = In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B) by A0, Lm5, A21, A14, A39;
hence Ext_eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = (In (((p . ((len p) -' 1)) * (q . ((len q) -' 1))),B)) * ((power B) . (x,(((len p) + (len q)) -' 2))) by Th17, A52; :: thesis: verum
end;
end;