let F be Field; for a, b, c being Element of (MPS F) ex d being Element of (MPS F) st
( a,b '||' c,d & a,c '||' b,d )
let a, b, c be Element of (MPS F); ex d being Element of (MPS F) st
( a,b '||' c,d & a,c '||' b,d )
consider e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1:
( e = a & f = b & g = c )
;
set h = (g + f) + (- e);
reconsider d = (g + f) + (- e) as Element of (MPS F) ;
A2:
[e,f,g,((g + f) + (- e))] = [a,b,c,d]
by A1;
take
d
; ( a,b '||' c,d & a,c '||' b,d )
( g + f = [((g `1) + (f `1)),((g `2) + (f `2)),((g `3) + (f `3))] & - e = [(- (e `1)),(- (e `2)),(- (e `3))] )
by Def1, Def3;
then A3:
(g + f) + (- e) = [(((g `1) + (f `1)) + (- (e `1))),(((g `2) + (f `2)) + (- (e `2))),(((g `3) + (f `3)) + (- (e `3)))]
by Th4;
then A4:
((g + f) + (- e)) `1 = ((g `1) + (f `1)) + (- (e `1))
by MCART_1:43;
A5:
((g + f) + (- e)) `3 = ((g `3) + (f `3)) + (- (e `3))
by A3, MCART_1:43;
then A6:
(((e `1) - (f `1)) * ((g `3) - (((g + f) + (- e)) `3))) - (((g `1) - (((g + f) + (- e)) `1)) * ((e `3) - (f `3))) = 0. F
by A4, Lm15;
A7:
(((e `1) - (g `1)) * ((f `3) - (((g + f) + (- e)) `3))) - (((f `1) - (((g + f) + (- e)) `1)) * ((e `3) - (g `3))) = 0. F
by A4, A5, Lm15;
A8:
((g + f) + (- e)) `2 = ((g `2) + (f `2)) + (- (e `2))
by A3, MCART_1:43;
then A9:
(((e `2) - (f `2)) * ((g `3) - (((g + f) + (- e)) `3))) - (((g `2) - (((g + f) + (- e)) `2)) * ((e `3) - (f `3))) = 0. F
by A5, Lm15;
(((e `1) - (f `1)) * ((g `2) - (((g + f) + (- e)) `2))) - (((g `1) - (((g + f) + (- e)) `1)) * ((e `2) - (f `2))) = 0. F
by A4, A8, Lm15;
hence
a,b '||' c,d
by A2, A6, A9, Th23; a,c '||' b,d
A10:
[e,g,f,((g + f) + (- e))] = [a,c,b,d]
by A1;
A11:
(((e `2) - (g `2)) * ((f `3) - (((g + f) + (- e)) `3))) - (((f `2) - (((g + f) + (- e)) `2)) * ((e `3) - (g `3))) = 0. F
by A8, A5, Lm15;
(((e `1) - (g `1)) * ((f `2) - (((g + f) + (- e)) `2))) - (((f `1) - (((g + f) + (- e)) `1)) * ((e `2) - (g `2))) = 0. F
by A4, A8, Lm15;
hence
a,c '||' b,d
by A10, A7, A11, Th23; verum