let L be non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr ; for p, q being Polynomial of L
for x being Element of L holds eval (((Leading-Monomial p) *' q),x) = (eval ((Leading-Monomial p),x)) * (eval (q,x))
let p1, q be Polynomial of L; for x being Element of L holds eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x))
let x be Element of L; eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x))
set p = Leading-Monomial p1;
defpred S1[ Nat] means for q being Polynomial of L st len q = $1 holds
eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x));
A1:
for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A2:
for
n being
Nat st
n < k holds
for
q being
Polynomial of
L st
len q = n holds
eval (
((Leading-Monomial p1) *' q),
x)
= (eval ((Leading-Monomial p1),x)) * (eval (q,x))
;
S1[k]
let q be
Polynomial of
L;
( len q = k implies eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x)) )
assume A3:
len q = k
;
eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x))
per cases
( len q <> 0 or len q = 0 )
;
suppose A4:
len q <> 0
;
eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x))set LMq =
Leading-Monomial q;
consider r being
Polynomial of
L such that A5:
len r < len q
and A6:
q = r + (Leading-Monomial q)
and
for
n being
Element of
NAT st
n < (len q) - 1 holds
r . n = q . n
by A4, Th16;
thus eval (
((Leading-Monomial p1) *' q),
x) =
eval (
(((Leading-Monomial p1) *' r) + ((Leading-Monomial p1) *' (Leading-Monomial q))),
x)
by A6, POLYNOM3:31
.=
(eval (((Leading-Monomial p1) *' r),x)) + (eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x))
by Th19
.=
((eval ((Leading-Monomial p1),x)) * (eval (r,x))) + (eval (((Leading-Monomial p1) *' (Leading-Monomial q)),x))
by A2, A3, A5
.=
((eval ((Leading-Monomial p1),x)) * (eval (r,x))) + ((eval ((Leading-Monomial p1),x)) * (eval ((Leading-Monomial q),x)))
by Lm3
.=
(eval ((Leading-Monomial p1),x)) * ((eval (r,x)) + (eval ((Leading-Monomial q),x)))
by VECTSP_1:def 7
.=
(eval ((Leading-Monomial p1),x)) * (eval (q,x))
by A6, Th19
;
verum end; end;
end;
A8:
for n being Nat holds S1[n]
from NAT_1:sch 4(A1);
len q = len q
;
hence
eval (((Leading-Monomial p1) *' q),x) = (eval ((Leading-Monomial p1),x)) * (eval (q,x))
by A8; verum