let F be Field; :: thesis: for e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds
( ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) )
let e, f, g, h be Element of [:the carrier of F,the carrier of F,the carrier of F:]; :: thesis: ( ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) )
A1: ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F & ( for K being Element of F holds
( not K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) or not K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) or not K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) ) implies ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) )

proof

assume that
A2: (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F and
A3: (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F and
A4: (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) )

now

A5: now

assume A6: (e `3 ) - (f `3 ) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) )
A7: (((g `3 ) - (h `3 )) * (((e `3 ) - (f `3 )) " )) * ((e `3 ) - (f `3 )) = ((g `3 ) - (h `3 )) * ((((e `3 ) - (f `3 )) " ) * ((e `3 ) - (f `3 ))) by GROUP_1:def 4
.= ((g `3 ) - (h `3 )) * (1_ F) by A6, VECTSP_1:def 22
.= (g `3 ) - (h `3 ) by VECTSP_1:def 19 ;
A8: (((g `3 ) - (h `3 )) * (((e `3 ) - (f `3 )) " )) * ((e `2 ) - (f `2 )) = (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) * (((e `3 ) - (f `3 )) " ) by GROUP_1:def 4
.= (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) * (((e `3 ) - (f `3 )) " ) by A4, Lm1
.= ((g `2 ) - (h `2 )) * (((e `3 ) - (f `3 )) * (((e `3 ) - (f `3 )) " )) by GROUP_1:def 4
.= ((g `2 ) - (h `2 )) * (1_ F) by A6, VECTSP_1:def 22
.= (g `2 ) - (h `2 ) by VECTSP_1:def 19 ;
(((g `3 ) - (h `3 )) * (((e `3 ) - (f `3 )) " )) * ((e `1 ) - (f `1 )) = (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) * (((e `3 ) - (f `3 )) " ) by GROUP_1:def 4
.= (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) * (((e `3 ) - (f `3 )) " ) by A3, Lm1
.= ((g `1 ) - (h `1 )) * (((e `3 ) - (f `3 )) * (((e `3 ) - (f `3 )) " )) by GROUP_1:def 4
.= ((g `1 ) - (h `1 )) * (1_ F) by A6, VECTSP_1:def 22
.= (g `1 ) - (h `1 ) by VECTSP_1:def 19 ;
hence ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) by A8, A7; :: thesis: verum

end;

A9: now

assume A10: (e `2 ) - (f `2 ) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) )
A11: (((g `2 ) - (h `2 )) * (((e `2 ) - (f `2 )) " )) * ((e `2 ) - (f `2 )) = ((g `2 ) - (h `2 )) * ((((e `2 ) - (f `2 )) " ) * ((e `2 ) - (f `2 ))) by GROUP_1:def 4
.= ((g `2 ) - (h `2 )) * (1_ F) by A10, VECTSP_1:def 22
.= (g `2 ) - (h `2 ) by VECTSP_1:def 19 ;
A12: (((g `2 ) - (h `2 )) * (((e `2 ) - (f `2 )) " )) * ((e `3 ) - (f `3 )) = (((e `2 ) - (f `2 )) " ) * (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) by GROUP_1:def 4
.= (((e `2 ) - (f `2 )) " ) * (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) by A4, Lm1
.= ((((e `2 ) - (f `2 )) " ) * ((e `2 ) - (f `2 ))) * ((g `3 ) - (h `3 )) by GROUP_1:def 4
.= ((g `3 ) - (h `3 )) * (1_ F) by A10, VECTSP_1:def 22
.= (g `3 ) - (h `3 ) by VECTSP_1:def 19 ;
(((g `2 ) - (h `2 )) * (((e `2 ) - (f `2 )) " )) * ((e `1 ) - (f `1 )) = (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) * (((e `2 ) - (f `2 )) " ) by GROUP_1:def 4
.= (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) * (((e `2 ) - (f `2 )) " ) by A2, Lm1
.= ((g `1 ) - (h `1 )) * (((e `2 ) - (f `2 )) * (((e `2 ) - (f `2 )) " )) by GROUP_1:def 4
.= ((g `1 ) - (h `1 )) * (1_ F) by A10, VECTSP_1:def 22
.= (g `1 ) - (h `1 ) by VECTSP_1:def 19 ;
hence ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) by A11, A12; :: thesis: verum

end;

now

assume A13: (e `1 ) - (f `1 ) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) )
A14: (((g `1 ) - (h `1 )) * (((e `1 ) - (f `1 )) " )) * ((e `1 ) - (f `1 )) = ((g `1 ) - (h `1 )) * ((((e `1 ) - (f `1 )) " ) * ((e `1 ) - (f `1 ))) by GROUP_1:def 4
.= ((g `1 ) - (h `1 )) * (1_ F) by A13, VECTSP_1:def 22
.= (g `1 ) - (h `1 ) by VECTSP_1:def 19 ;
A15: (((g `1 ) - (h `1 )) * (((e `1 ) - (f `1 )) " )) * ((e `3 ) - (f `3 )) = (((e `1 ) - (f `1 )) " ) * (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) by GROUP_1:def 4
.= (((e `1 ) - (f `1 )) " ) * (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) by A3, Lm1
.= ((((e `1 ) - (f `1 )) " ) * ((e `1 ) - (f `1 ))) * ((g `3 ) - (h `3 )) by GROUP_1:def 4
.= ((g `3 ) - (h `3 )) * (1_ F) by A13, VECTSP_1:def 22
.= (g `3 ) - (h `3 ) by VECTSP_1:def 19 ;
(((g `1 ) - (h `1 )) * (((e `1 ) - (f `1 )) " )) * ((e `2 ) - (f `2 )) = (((e `1 ) - (f `1 )) " ) * (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) by GROUP_1:def 4
.= (((e `1 ) - (f `1 )) " ) * (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) by A2, Lm1
.= ((((e `1 ) - (f `1 )) " ) * ((e `1 ) - (f `1 ))) * ((g `2 ) - (h `2 )) by GROUP_1:def 4
.= ((g `2 ) - (h `2 )) * (1_ F) by A13, VECTSP_1:def 22
.= (g `2 ) - (h `2 ) by VECTSP_1:def 19 ;
hence ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) by A14, A15; :: thesis: verum

end;

hence ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) by A9, A5; :: thesis: verum

end;

hence ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) ; :: thesis: verum

end;

( ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) implies ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) )

proof

A16: now

given K being Element of F such that A17: K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) and
A18: ( K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) ; :: thesis: ( ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) implies ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) )
A19: (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = ((K * ((e `2 ) - (f `2 ))) * ((e `3 ) - (f `3 ))) - ((K * ((e `2 ) - (f `2 ))) * ((e `3 ) - (f `3 ))) by A18, GROUP_1:def 4;
( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = ((K * ((e `1 ) - (f `1 ))) * ((e `2 ) - (f `2 ))) - ((K * ((e `1 ) - (f `1 ))) * ((e `2 ) - (f `2 ))) & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = ((K * ((e `1 ) - (f `1 ))) * ((e `3 ) - (f `3 ))) - ((K * ((e `1 ) - (f `1 ))) * ((e `3 ) - (f `3 ))) ) by A17, A18, GROUP_1:def 4;
hence ( ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) implies ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) ) by A19, RLVECT_1:28; :: thesis: verum

end;

A20: now

assume that
A21: (e `1 ) - (f `1 ) = 0. F and
A22: (e `2 ) - (f `2 ) = 0. F and
A23: (e `3 ) - (f `3 ) = 0. F ; :: thesis: ( ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) implies ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) )
A24: ((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 )) = 0. F by A23, VECTSP_1:39;
( ((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 )) = 0. F & ((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 )) = 0. F ) by A21, VECTSP_1:39;
hence ( ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) implies ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) ) by A21, A22, A23, A24, RLVECT_1:28; :: thesis: verum

end;

assume ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) ; :: thesis: ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F )
hence ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) by A20, A16; :: thesis: verum

end;

hence ( ( (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) ) by A1; :: thesis: verum