let F be Field; :: thesis: for a, b, c, d being Element of (MPS F) st (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c
let a, b, c, d be Element of (MPS F); :: thesis: ( (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies a,b '||' a,c )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: b,c '||' a,d and
A3: a,b '||' c,d and
A4: a,c '||' b,d ; :: thesis: a,b '||' a,c
assume A5: not a,b '||' a,c ; :: thesis: contradiction
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A6: [[b,c],[a,d]] = [[i,j],[k,l]] and
A7: ( ex L being Element of F st
( L * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & L * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & L * ((i `3_3) - (j `3_3)) = (k `3_3) - (l `3_3) ) or ( (i `1_3) - (j `1_3) = 0. F & (i `2_3) - (j `2_3) = 0. F & (i `3_3) - (j `3_3) = 0. F ) ) by A2, Th2;
A8: ( b = i & c = j ) by A6, MCART_1:93;
A9: ( a = k & d = l ) by A6, MCART_1:93;
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A10: [[a,b],[c,d]] = [[e,f],[g,h]] and
( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A3, Th2;
A11: b = f by A10, MCART_1:93;
A12: d = h by A10, MCART_1:93;
A13: c = g by A10, MCART_1:93;
A14: a = e by A10, MCART_1:93;
then A15: [[a,b],[a,c]] = [[e,f],[e,g]] by A10, A11, MCART_1:93;
( f = [(f `1_3),(f `2_3),(f `3_3)] & g = [(g `1_3),(g `2_3),(g `3_3)] ) ;
then ( i `1_3 <> j `1_3 or i `2_3 <> j `2_3 or i `3_3 <> j `3_3 ) by A5, A11, A13, A15, A8, Th3;
then consider L being Element of F such that
A16: L * ((f `1_3) - (g `1_3)) = (e `1_3) - (h `1_3) and
A17: L * ((f `2_3) - (g `2_3)) = (e `2_3) - (h `2_3) and
A18: L * ((f `3_3) - (g `3_3)) = (e `3_3) - (h `3_3) by A14, A11, A13, A12, A7, A8, A9, Lm2;
h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) by A3, A4, A5, A10, Th5;
then A19: (L - (1_ F)) * ((e `2_3) - (g `2_3)) = (L + (1_ F)) * ((e `2_3) - (f `2_3)) by A17, Lm9;
h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) by A3, A4, A5, A10, Th5;
then A20: (L - (1_ F)) * ((e `3_3) - (g `3_3)) = (L + (1_ F)) * ((e `3_3) - (f `3_3)) by A18, Lm9;
h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) by A3, A4, A5, A10, Th5;
then (L - (1_ F)) * ((e `1_3) - (g `1_3)) = (L + (1_ F)) * ((e `1_3) - (f `1_3)) by A16, Lm9;
then ( L + (1_ F) = 0. F & L - (1_ F) = 0. F ) by A5, A15, A19, A20, Th4;
then (L + (1_ F)) - (L - (1_ F)) = (0. F) + (- (0. F)) by RLVECT_1:def 11;
then (L + (1_ F)) - (L - (1_ F)) = 0. F by RLVECT_1:5;
then (L + (1_ F)) + (- (L - (1_ F))) = 0. F by RLVECT_1:def 11;
then (L + (1_ F)) + ((1_ F) + (- L)) = 0. F by RLVECT_1:33;
then ((L + (1_ F)) + (1_ F)) + (- L) = 0. F by RLVECT_1:def 3;
then (((1_ F) + (1_ F)) + L) + (- L) = 0. F by RLVECT_1:def 3;
then ((1_ F) + (1_ F)) + (L + (- L)) = 0. F by RLVECT_1:def 3;
then ((1_ F) + (1_ F)) + (0. F) = 0. F by RLVECT_1:5;
hence contradiction by A1, RLVECT_1:4; :: thesis: verum