let R be domRing; :: thesis: for x, y being Element of the carrier of (Polynom-Ring R) st not x is constant holds
(Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y))
let x, y be Element of the carrier of (Polynom-Ring R); :: thesis: ( not x is constant implies (Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y)) )
assume A1: not x is constant ; :: thesis: (Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y))
defpred S₁[ Nat] means for f, g, f0, g0 being Element of the carrier of (Polynom-Ring R) st f0 = f & g0 = g & (deg f0) - 1 = $1 holds
(Der1 R) . (f0 * g0) = (((Der1 R) . f0) * g0) + (f0 * ((Der1 R) . g0));
A2: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
for f, g being Element of the carrier of (Polynom-Ring R) st (deg f) - 1 = k holds
(Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

proof

let f, g be Element of the carrier of (Polynom-Ring R); :: thesis: ( (deg f) - 1 = k implies (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) )
assume A4: (deg f) - 1 = k ; :: thesis: (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))
reconsider f1 = f, g1 = g as Polynomial of R ;
A5: not f1 is constant by A4;
A6: 1 + 1 <= (1 + 1) + k by NAT_1:11;
consider u1 being Polynomial of R such that
A7: ( len u1 < len f1 & f1 = u1 + (LM f1) & ( for i being Element of NAT st i < (len f1) - 1 holds
u1 . i = f1 . i ) ) by A4, A6, POLYNOM4:16;
reconsider u = u1, an = anpoly ((1. R),1) as Element of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider df1 = (Der1 R) . f, dg1 = (Der1 R) . g as Polynomial of R ;
A8: LC f1 = f1 . (deg f1) by A4, A6, XXREAL_0:2, XREAL_1:233;
reconsider f1 = f1 as non constant Polynomial of R by A5;
A9: LM f1 = ((LC f1) * (anpoly ((1. R),((deg f1) -' 1)))) *' (anpoly ((1. R),1)) by A8, Lm4;
A10: len f1 = (deg f1) + 1 ;
not f1 . (deg f1) is zero by A10, ALGSEQ_1:10;
then reconsider a = f1 . (deg f1) as non zero Element of R ;
reconsider h1 = (LC f1) * (anpoly ((1. R),((deg f1) -' 1))) as Polynomial of R ;
A11: deg h1 = deg (anpoly ((1. R),((deg f1) -' 1))) by RING_5:4
.= (deg f1) -' 1 by FIELD_1:4 ;
(Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g))

proof

f1 = u1 + (h1 *' (anpoly ((1. R),1))) by A7, A8, Lm4;
then A12: f * g = (u1 + (h1 *' (anpoly ((1. R),1)))) *' g1 by POLYNOM3:def 10
.= (u1 *' g1) + ((h1 *' (anpoly ((1. R),1))) *' g1) by POLYNOM3:32 ;
A13: deg h1 = (k + 1) - 1 by A4, A11, NAT_1:11, XREAL_1:233;
reconsider h = h1, ang = (anpoly ((1. R),1)) *' g1, an = anpoly ((1. R),1), t = (anpoly ((1. R),1)) *' g1, LMf = LM f1 as Element of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider t1 = (anpoly ((1. R),1)) *' g1 as Polynomial of R ;
reconsider dan1 = (Der1 R) . an, df1 = (Der1 R) . f, dg1 = (Der1 R) . g, du1 = (Der1 R) . u, dh1 = (Der1 R) . h as Polynomial of R ;
A14: ( u1 *' g1 = u * g & h1 *' t1 = h * t ) by POLYNOM3:def 10;
f * g = (u1 *' g1) + (h1 *' ((anpoly ((1. R),1)) *' g1)) by A12, POLYNOM3:33;
then A15: f * g = (u * g) + (h * t) by A14, POLYNOM3:def 10
.= (u * g) + (h * (an * g)) by POLYNOM3:def 10 ;
A16: deg u1 < deg f1 by A7, XREAL_1:9;
A17: (Der1 R) . (u * g) = (((Der1 R) . u) * g) + (u * ((Der1 R) . g))

proof

per cases ( not u is constant or u is constant ) ;

suppose not u is constant ; :: thesis: (Der1 R) . (u * g) = (((Der1 R) . u) * g) + (u * ((Der1 R) . g))

then reconsider n1 = (deg u1) - 1 as Nat ;
n1 < k by A4, A16, XREAL_1:9;
hence (Der1 R) . (u * g) = (((Der1 R) . u) * g) + (u * ((Der1 R) . g)) by A3; :: thesis: verum

end;

suppose u is constant ; :: thesis: (Der1 R) . (u * g) = (((Der1 R) . u) * g) + (u * ((Der1 R) . g))

hence (Der1 R) . (u * g) = (((Der1 R) . u) * g) + (u * ((Der1 R) . g)) by Th34; :: thesis: verum

end;

end;

end;

A21: (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((Der1 R) . (an * g)))

proof

per cases ( not h is constant or h is constant ) ;

suppose not h is constant ; :: thesis: (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((Der1 R) . (an * g)))

then reconsider m1 = (deg h1) - 1 as Nat ;
m1 < k by XREAL_1:44, A13;
hence (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((Der1 R) . (an * g))) by A3; :: thesis: verum

end;

suppose h is constant ; :: thesis: (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((Der1 R) . (an * g)))

hence (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((Der1 R) . (an * g))) by Th34; :: thesis: verum

end;

end;

end;

reconsider s1 = ((Der1 R) . an) * h, t1 = an * ((Der1 R) . h) as Polynomial of R by POLYNOM3:def 10;
A25: (Der1 R) . (h * an) = (((Der1 R) . h) * an) + (h * ((Der1 R) . an)) by Th32;
A26: ((Der1 R) . h) * an = dh1 *' (anpoly ((1. R),1)) by POLYNOM3:def 10;
A27: ((Der1 R) . h) * (an * g) = (((Der1 R) . h) * an) * g by GROUP_1:def 3
.= (dh1 *' (anpoly ((1. R),1))) *' g1 by A26, POLYNOM3:def 10 ;
A28: (Der1 R) . (f * g) = ((((Der1 R) . u) * g) + (u * ((Der1 R) . g))) + ((Der1 R) . (h * (an * g))) by A17, A15, VECTSP_1:def 20;
( u * ((Der1 R) . g) = u1 *' dg1 & ((Der1 R) . u) * g = du1 *' g1 ) by POLYNOM3:def 10;
then A30: (((Der1 R) . u) * g) + (u * ((Der1 R) . g)) = (du1 *' g1) + (u1 *' dg1) by POLYNOM3:def 10;
( ((Der1 R) . an) * g = dan1 *' g1 & an * ((Der1 R) . g) = (anpoly ((1. R),1)) *' dg1 ) by POLYNOM3:def 10;
then (((Der1 R) . an) * g) + (an * ((Der1 R) . g)) = (dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1) by POLYNOM3:def 10;
then A32: h * ((((Der1 R) . an) * g) + (an * ((Der1 R) . g))) = h1 *' ((dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1)) by POLYNOM3:def 10;
A33: (Der1 R) . (h * (an * g)) = (((Der1 R) . h) * (an * g)) + (h * ((((Der1 R) . an) * g) + (an * ((Der1 R) . g)))) by Th32, A21
.= ((dh1 *' (anpoly ((1. R),1))) *' g1) + (h1 *' ((dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1))) by A32, A27, POLYNOM3:def 10 ;
h * ((Der1 R) . an) = h1 *' dan1 by POLYNOM3:def 10;
then A34: (((Der1 R) . h) * an) + (h * ((Der1 R) . an)) = (dh1 *' (anpoly ((1. R),1))) + (h1 *' dan1) by A26, POLYNOM3:def 10;
A35: LM f1 = h * an by A9, POLYNOM3:def 10;
f1 = u + LMf by A7, POLYNOM3:def 10;
then A36: (Der1 R) . f = ((Der1 R) . u) + ((((Der1 R) . h) * an) + (h * ((Der1 R) . an))) by A25, A35, VECTSP_1:def 20
.= du1 + ((dh1 *' (anpoly ((1. R),1))) + (h1 *' dan1)) by A34, POLYNOM3:def 10
.= (du1 + (dh1 *' (anpoly ((1. R),1)))) + (h1 *' dan1) by POLYNOM3:26 ;
A37: ( ((Der1 R) . f) * g = df1 *' g1 & f * ((Der1 R) . g) = f1 *' dg1 ) by POLYNOM3:def 10;
A38: f1 = u1 + (h1 *' (anpoly ((1. R),1))) by A7, A8, Lm4;
(Der1 R) . (f * g) = ((du1 *' g1) + (u1 *' dg1)) + (((dh1 *' (anpoly ((1. R),1))) *' g1) + (h1 *' ((dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1)))) by A28, A30, A33, POLYNOM3:def 10
.= (((du1 *' g1) + (u1 *' dg1)) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + (h1 *' ((dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1))) by POLYNOM3:26
.= (((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + (u1 *' dg1)) + (h1 *' ((dan1 *' g1) + ((anpoly ((1. R),1)) *' dg1))) by POLYNOM3:26
.= (((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + (u1 *' dg1)) + ((h1 *' (dan1 *' g1)) + (h1 *' ((anpoly ((1. R),1)) *' dg1))) by POLYNOM3:31
.= ((((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + (u1 *' dg1)) + (h1 *' (dan1 *' g1))) + (h1 *' ((anpoly ((1. R),1)) *' dg1)) by POLYNOM3:26
.= ((((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + (u1 *' dg1)) + ((h1 *' dan1) *' g1)) + (h1 *' ((anpoly ((1. R),1)) *' dg1)) by POLYNOM3:33
.= ((((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + ((h1 *' dan1) *' g1)) + (u1 *' dg1)) + (h1 *' ((anpoly ((1. R),1)) *' dg1)) by POLYNOM3:26
.= ((((du1 *' g1) + ((dh1 *' (anpoly ((1. R),1))) *' g1)) + ((h1 *' dan1) *' g1)) + (u1 *' dg1)) + ((h1 *' (anpoly ((1. R),1))) *' dg1) by POLYNOM3:33
.= ((((du1 + (dh1 *' (anpoly ((1. R),1)))) *' g1) + ((h1 *' dan1) *' g1)) + (u1 *' dg1)) + ((h1 *' (anpoly ((1. R),1))) *' dg1) by POLYNOM3:32
.= ((((du1 + (dh1 *' (anpoly ((1. R),1)))) + (h1 *' dan1)) *' g1) + (u1 *' dg1)) + ((h1 *' (anpoly ((1. R),1))) *' dg1) by POLYNOM3:32
.= (((du1 + (dh1 *' (anpoly ((1. R),1)))) + (h1 *' dan1)) *' g1) + ((u1 *' dg1) + ((h1 *' (anpoly ((1. R),1))) *' dg1)) by POLYNOM3:26
.= (df1 *' g1) + (f1 *' dg1) by A38, A36, POLYNOM3:32
.= (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) by A37, POLYNOM3:def 10 ;
hence (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) ; :: thesis: verum

end;

hence (Der1 R) . (f * g) = (((Der1 R) . f) * g) + (f * ((Der1 R) . g)) ; :: thesis: verum

end;

hence S₁[k] ; :: thesis: verum

end;

A39: for n being Nat holds S₁[n] from NAT_1:sch 4(A2);
ex n being Nat st (deg x) - 1 = n by A1;
hence (Der1 R) . (x * y) = (((Der1 R) . x) * y) + (x * ((Der1 R) . y)) by A39; :: thesis: verum