let F be Field; :: thesis: 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); :: thesis: 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 ; :: thesis: ( 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:47;
A5: ((g + f) + (- e)) `3 = ((g `3 ) + (f `3 )) + (- (e `3 )) by A3, MCART_1:47;
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:47;
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; :: thesis: 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; :: thesis: verum