let L be non empty right_complementable add-associative right_zeroed distributive unital associative doubleLoopStr ; 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; ( 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 that
A1:
len p > 0
and
A2:
len q > 0
; 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)))
A3:
len q >= 0 + 1
by A2, NAT_1:13;
then A4:
(len q) - 1 >= 0
by XREAL_1:19;
A5:
len p >= 0 + 1
by A1, NAT_1:13;
then
(len p) - 1 >= 0
by XREAL_1:19;
then A6:
(len p) - 1 = (len p) -' 1
by XREAL_0:def 2;
A7:
(len p) + (len q) >= 0 + (1 + 1)
by A5, A3, XREAL_1:7;
then A8:
((len p) + (len q)) - 1 >= 1
by XREAL_1:19;
then reconsider i1 = ((len p) + (len q)) - 1 as Element of NAT by INT_1:3;
A9:
(i1 -' 1) + 1 = i1
by A8, XREAL_1:235;
set LMp = Leading-Monomial p;
set LMq = Leading-Monomial q;
let x be Element of L; eval (((Leading-Monomial p) *' (Leading-Monomial q)),x) = ((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2)))
consider F being FinSequence of the carrier of L such that
A10:
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 = (((Leading-Monomial p) *' (Leading-Monomial q)) . (n -' 1)) * ((power L) . (x,(n -' 1)))
by Def2;
consider r being FinSequence of the carrier of L 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 A4, XREAL_1:7;
then
len p in Seg (len r)
by A5, A9, A13, FINSEQ_1:1;
then A16:
len p in dom r
by FINSEQ_1:def 3;
((len p) + ((len q) - 1)) - (len p) >= 0
by A3, XREAL_1:19;
then i1 -' (len p) =
((len p) + ((len q) - 1)) - (len p)
by XREAL_0:def 2
.=
(len q) -' 1
by A4, 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;
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 Def1
.=
(p . ((len p) -' 1)) * (q . ((len q) -' 1))
by Def1
;
A22:
(len q) - 1 = (len q) -' 1
by A4, XREAL_0:def 2;
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. L or ((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L )
;
suppose
((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) <> 0. L
;
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 A11, ALGSEQ_1:8;
then
len F >= i1
by A9, NAT_1:13;
then
i1 in Seg (len F)
by A8, FINSEQ_1:1;
then A38:
i1 in dom F
by FINSEQ_1:def 3;
hence eval (
((Leading-Monomial p) *' (Leading-Monomial q)),
x) =
F /. i1
by A10, A23, POLYNOM2:3
.=
F . i1
by A38, PARTFUN1:def 6
.=
((p . ((len p) -' 1)) * (q . ((len q) -' 1))) * ((power L) . (x,(((len p) + (len q)) -' 2)))
by A12, A14, A37, A21, A38
;
verum end; suppose A39:
((Leading-Monomial p) *' (Leading-Monomial q)) . (i1 -' 1) = 0. L
;
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 for j being Nat st j >= 0 holds
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. Llet j be
Nat;
( j >= 0 implies ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L )assume
j >= 0
;
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L
j in NAT
by ORDINAL1:def 12;
then consider r1 being
FinSequence of the
carrier of
L 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 ((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. Lper cases
( j = i1 -' 1 or j <> i1 -' 1 )
;
suppose A43:
j <> i1 -' 1
;
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. Lnow for k being Element of NAT st k in dom r1 holds
r1 . k = 0. Llet k be
Element of
NAT ;
( k in dom r1 implies r1 . b1 = 0. L )assume A44:
k in dom r1
;
r1 . b1 = 0. Lper cases
( k -' 1 <> (len p) -' 1 or k -' 1 = (len p) -' 1 )
;
suppose A46:
k -' 1
= (len p) -' 1
;
r1 . b1 = 0. LA47:
k in Seg (len r1)
by A44, FINSEQ_1:def 3;
then
0 + 1
<= k
by FINSEQ_1:1;
then
k - 1
>= 0
by XREAL_1:19;
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. L)
by A22, A9, A49, A50, Def1
.=
0. L
;
verum end; end; end; hence
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L
by A41, POLYNOM3:1;
verum end; end; end; hence
((Leading-Monomial p) *' (Leading-Monomial q)) . j = 0. L
;
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
(Leading-Monomial p) *' (Leading-Monomial q) = 0_. L
by Th5;
then
eval (
((Leading-Monomial p) *' (Leading-Monomial q)),
x)
= 0. L
by Th17;
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 A14, A21, A39;
verum end; end;