let F be Field; for a, b, c, d, e, f being Element of F st ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F holds
((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F
let a, b, c, d, e, f be Element of F; ( ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F implies ((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F )
assume A1:
((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F
; ((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F
A2:
( (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d)))) & (a - e) * (c - f) = (a * c) + ((- (a * f)) + (- (e * (c - f)))) )
by Lm9;
( (b - a) * (f - d) = (b * f) + ((- (b * d)) + (- (a * (f - d)))) & (b - e) * (f - c) = (b * f) + ((- (b * c)) + (- (e * (f - c)))) )
by Lm9;
hence ((b - a) * (f - d)) - ((b - e) * (f - c)) =
((- (b * d)) + (- (a * (f - d)))) - ((- (b * c)) + (- (e * (f - c))))
by Lm11
.=
((- (b * d)) + (- ((a * f) - (a * d)))) - ((- (b * c)) + (- (e * (f - c))))
by VECTSP_1:11
.=
((- (b * d)) + ((- (a * f)) + (a * d))) - ((- (b * c)) + (- (e * (f - c))))
by RLVECT_1:33
.=
(((- (b * d)) + (a * d)) + (- (a * f))) - ((- (b * c)) + (- (e * (f - c))))
by RLVECT_1:def 3
.=
(((a * d) + (- (b * d))) + (- (a * f))) + (- ((- (b * c)) + (- (e * (f - c)))))
by RLVECT_1:def 11
.=
(((a * d) + (- (b * d))) + (- (a * f))) + ((- (- (b * c))) + (- (- (e * (f - c)))))
by RLVECT_1:31
.=
(((a * d) + (- (b * d))) + (- (a * f))) + ((b * c) + (- (- (e * (f - c)))))
by RLVECT_1:17
.=
(((a * d) + (- (b * d))) + (- (a * f))) + ((b * c) + (e * (f - c)))
by RLVECT_1:17
.=
(((a * d) + (- (b * d))) + ((- (a * f)) + (b * c))) + (e * (f - c))
by Lm10
.=
(((a * d) + (- (b * d))) + (b * c)) + ((- (a * f)) + (e * (f - c)))
by Lm10
.=
((a * d) + ((- (b * d)) + (b * c))) + ((- (a * f)) + (e * (f - c)))
by RLVECT_1:def 3
.=
((a * d) + ((b * c) - (b * d))) + ((- (a * f)) + (e * (f - c)))
by RLVECT_1:def 11
.=
((a * d) + (b * (c - d))) + ((- (a * f)) + (e * (f - c)))
by VECTSP_1:11
.=
(- ((- (a * d)) + (- (b * (c - d))))) + ((- (a * f)) + (e * (f - c)))
by Lm12
.=
(- ((- (a * d)) + (- (b * (c - d))))) + (- ((- (- (a * f))) + (- (e * (f - c)))))
by Lm12
.=
(- ((- (a * d)) + (- (b * (c - d))))) + (- ((a * f) + (- (e * (f - c)))))
by RLVECT_1:17
.=
- (((- (a * d)) + (- (b * (c - d)))) + ((a * f) + (- (e * (f - c)))))
by RLVECT_1:31
.=
- (((- (a * d)) + (- (b * (c - d)))) + (- ((- (a * f)) + (- (- (e * (f - c)))))))
by Lm12
.=
- (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- (- (e * (f - c))))))
by RLVECT_1:def 11
.=
- (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- ((- (f - c)) * e))))
by VECTSP_1:9
.=
- (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- (e * (c - f)))))
by Lm1
.=
- (0. F)
by A1, A2, Lm11
.=
0. F
by RLVECT_1:12
;
verum