let R be non degenerated comRing; :: thesis: for D being Derivation of R
for x, y, z being Element of R st z * y = 1. R holds
(y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))
let D be Derivation of R; :: thesis: for x, y, z being Element of R st z * y = 1. R holds
(y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))
let x, y, z be Element of R; :: thesis: ( z * y = 1. R implies (y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y)) )
assume A1: z * y = 1. R ; :: thesis: (y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y))
reconsider c = x * z as Element of R ;
reconsider d = c * (D . y) as Element of R ;
c * y = x * (1. R) by A1, GROUP_1:def 3
.= x ;
then D . x = (c * (D . y)) + (y * (D . c)) by Def1;
then A2: y * (D . c) = (D . x) - (c * (D . y)) by VECTSP_2:2
.= (D . x) + (- d) ;
A3: y * (c * (D . y)) = (y * (z * x)) * (D . y) by GROUP_1:def 3
.= ((1. R) * x) * (D . y) by A1, GROUP_1:def 3
.= x * (D . y) ;
y |^ 2 = y |^ (1 + 1)
.= (y |^ 1) * (y |^ 1) by BINOM:10
.= y * (y |^ 1) by BINOM:8
.= y * y by BINOM:8 ;
then (y |^ 2) * (D . c) = y * ((D . x) + (- d)) by A2, GROUP_1:def 3
.= (y * (D . x)) + (y * (- d)) by VECTSP_1:def 2
.= (y * (D . x)) - (x * (D . y)) by A3, VECTSP_1:8 ;
hence (y |^ 2) * (D . (x * z)) = (y * (D . x)) - (x * (D . y)) ; :: thesis: verum