let F be Field; for b, c, a, 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 b, c, a, d be Element of (MPS F); ( (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
; a,b '||' a,c
assume A5:
not a,b '||' a,c
; 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) - (j `1)) = (k `1) - (l `1) & L * ((i `2) - (j `2)) = (k `2) - (l `2) & L * ((i `3) - (j `3)) = (k `3) - (l `3) ) or ( (i `1) - (j `1) = 0. F & (i `2) - (j `2) = 0. F & (i `3) - (j `3) = 0. F ) )
by A2, Th2;
A8:
( b = i & c = j )
by A6, MCART_1:29;
A9:
( a = k & d = l )
by A6, MCART_1:29;
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) - (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 A3, Th2;
A11:
b = f
by A10, MCART_1:29;
A12:
d = h
by A10, MCART_1:29;
A13:
c = g
by A10, MCART_1:29;
A14:
a = e
by A10, MCART_1:29;
then A15:
[a,b,a,c] = [e,f,e,g]
by A10, A11, MCART_1:29;
( f = [(f `1),(f `2),(f `3)] & g = [(g `1),(g `2),(g `3)] )
by MCART_1:44;
then
( i `1 <> j `1 or i `2 <> j `2 or i `3 <> j `3 )
by A5, A11, A13, A15, A8, Th3;
then consider L being Element of F such that
A16:
L * ((f `1) - (g `1)) = (e `1) - (h `1)
and
A17:
L * ((f `2) - (g `2)) = (e `2) - (h `2)
and
A18:
L * ((f `3) - (g `3)) = (e `3) - (h `3)
by A14, A11, A13, A12, A7, A8, A9, Lm2;
h `2 = ((f `2) + (g `2)) - (e `2)
by A3, A4, A5, A10, Th5;
then A19:
(L - (1_ F)) * ((e `2) - (g `2)) = (L + (1_ F)) * ((e `2) - (f `2))
by A17, Lm9;
h `3 = ((f `3) + (g `3)) - (e `3)
by A3, A4, A5, A10, Th5;
then A20:
(L - (1_ F)) * ((e `3) - (g `3)) = (L + (1_ F)) * ((e `3) - (f `3))
by A18, Lm9;
h `1 = ((f `1) + (g `1)) - (e `1)
by A3, A4, A5, A10, Th5;
then
(L - (1_ F)) * ((e `1) - (g `1)) = (L + (1_ F)) * ((e `1) - (f `1))
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; verum