let F be Field; :: thesis: for a, b, c, d, e, h being Element of F st a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
let a, b, c, d, e, h be Element of F; :: thesis: ( a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume that
A1: a <> 0. F and
A2: (a * e) - (d * b) = 0. F and
A3: (a * c) - (h * b) = 0. F ; :: thesis: (d * c) - (h * e) = 0. F
c = (h * b) * (a ") by A1, A3, VECTSP_1:30;
then c = h * (b * (a ")) by GROUP_1:def 3;
then A4: d * c = (d * h) * (b * (a ")) by GROUP_1:def 3;
e = (d * b) * (a ") by A1, A2, VECTSP_1:30;
then e = d * (b * (a ")) by GROUP_1:def 3;
then h * e = (h * d) * (b * (a ")) by GROUP_1:def 3;
hence (d * c) - (h * e) = 0. F by A4, RLVECT_1:15; :: thesis: verum