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_3) + (f `1_3)),((g `2_3) + (f `2_3)),((g `3_3) + (f `3_3))] & - e = [(- (e `1_3)),(- (e `2_3)),(- (e `3_3))] ) by Def1, Def3;
then A3: (g + f) + (- e) = [(((g `1_3) + (f `1_3)) + (- (e `1_3))),(((g `2_3) + (f `2_3)) + (- (e `2_3))),(((g `3_3) + (f `3_3)) + (- (e `3_3)))] by Th2;
then A4: ((g + f) + (- e)) `1_3 = ((g `1_3) + (f `1_3)) + (- (e `1_3)) ;
A5: ((g + f) + (- e)) `3_3 = ((g `3_3) + (f `3_3)) + (- (e `3_3)) by A3;
then A6: (((e `1_3) - (f `1_3)) * ((g `3_3) - (((g + f) + (- e)) `3_3))) - (((g `1_3) - (((g + f) + (- e)) `1_3)) * ((e `3_3) - (f `3_3))) = 0. F by A4, Lm15;
A7: (((e `1_3) - (g `1_3)) * ((f `3_3) - (((g + f) + (- e)) `3_3))) - (((f `1_3) - (((g + f) + (- e)) `1_3)) * ((e `3_3) - (g `3_3))) = 0. F by A4, A5, Lm15;
A8: ((g + f) + (- e)) `2_3 = ((g `2_3) + (f `2_3)) + (- (e `2_3)) by A3;
then A9: (((e `2_3) - (f `2_3)) * ((g `3_3) - (((g + f) + (- e)) `3_3))) - (((g `2_3) - (((g + f) + (- e)) `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by A5, Lm15;
(((e `1_3) - (f `1_3)) * ((g `2_3) - (((g + f) + (- e)) `2_3))) - (((g `1_3) - (((g + f) + (- e)) `1_3)) * ((e `2_3) - (f `2_3))) = 0. F by A4, A8, Lm15;
hence a,b '||' c,d by A2, A6, A9, Th12; :: thesis: a,c '||' b,d
A10: [[e,g],[f,((g + f) + (- e))]] = [[a,c],[b,d]] by A1;
A11: (((e `2_3) - (g `2_3)) * ((f `3_3) - (((g + f) + (- e)) `3_3))) - (((f `2_3) - (((g + f) + (- e)) `2_3)) * ((e `3_3) - (g `3_3))) = 0. F by A8, A5, Lm15;
(((e `1_3) - (g `1_3)) * ((f `2_3) - (((g + f) + (- e)) `2_3))) - (((f `1_3) - (((g + f) + (- e)) `1_3)) * ((e `2_3) - (g `2_3))) = 0. F by A4, A8, Lm15;
hence a,c '||' b,d by A10, A7, A11, Th12; :: thesis: verum