let r1, r2 be Real; :: thesis: for d, e, f, g, h, i being Real st ( r1 <> 0 or r2 <> 0 ) & ((r1 * d) * e) + ((r2 * d) * f) = ((r1 + r2) * e) * f & ((r1 * g) * h) + ((r2 * g) * i) = ((r1 + r2) * h) * i holds
((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)
let d, e, f, g, h, i be Real; :: thesis: ( ( r1 <> 0 or r2 <> 0 ) & ((r1 * d) * e) + ((r2 * d) * f) = ((r1 + r2) * e) * f & ((r1 * g) * h) + ((r2 * g) * i) = ((r1 + r2) * h) * i implies ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h) )
assume that
A1: ( r1 <> 0 or r2 <> 0 ) and
A2: ((r1 * d) * e) + ((r2 * d) * f) = ((r1 + r2) * e) * f and
A3: ((r1 * g) * h) + ((r2 * g) * i) = ((r1 + r2) * h) * i ; :: thesis: ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)
per cases ( r1 <> 0 or r2 <> 0 ) by A1;
suppose A4: r1 <> 0 ; :: thesis: ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)
A5: (i * (h - g)) * (((e * (d - f)) * r1) + ((f * (d - e)) * r2)) = (i * (h - g)) * 0 by A2;
(f * (e - d)) * (((h * (g - i)) * r1) + ((i * (g - h)) * r2)) = (f * (e - d)) * 0 by A3;
then (((i * (g - h)) * e) * (d - f)) * r1 = (((f * (d - e)) * h) * (g - i)) * r1 by A5;
hence ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h) by A4, XCMPLX_1:5; :: thesis: verum
end;
suppose A6: r2 <> 0 ; :: thesis: ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)
(h * (g - i)) * (((e * (d - f)) * r1) + ((f * (d - e)) * r2)) = (h * (g - i)) * 0 by A2;
then A7: (((h * (g - i)) * e) * (d - f)) * r1 = - ((((h * (g - i)) * f) * (d - e)) * r2) ;
(e * (d - f)) * (((h * (g - i)) * r1) + ((i * (g - h)) * r2)) = (e * (d - f)) * 0 by A3;
then (((e * (d - f)) * h) * (g - i)) * r1 = - ((((e * (d - f)) * i) * (g - h)) * r2) ;
hence ((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h) by A7, A6, XCMPLX_1:5; :: thesis: verum
end;
end;