let F be Field; :: thesis: not for a, b, c being Element of (MPS F) holds a,b '||' a,c
consider e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: e = [(1_ F),(1_ F),(0. F)] and
A2: f = [(- (0. F)),(1_ F),(0. F)] and
A3: g = [(1_ F),(- (0. F)),(0. F)] ;
A4: ( f `1_3 = - (0. F) & f `2_3 = 1_ F ) by A2;
A5: ( g `1_3 = 1_ F & g `2_3 = - (0. F) ) by A3;
the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] by PARSP_1:10;
then consider a, b, c being Element of (MPS F) such that
A6: [[a,b],[a,c]] = [[e,f],[e,g]] ;
take a ; :: thesis: not for b, c being Element of (MPS F) holds a,b '||' a,c
take b ; :: thesis: not for c being Element of (MPS F) holds a,b '||' a,c
take c ; :: thesis: not a,b '||' a,c
( e `1_3 = 1_ F & e `2_3 = 1_ F ) by A1;
then A7: (((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3))) - (((e `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3))) = (((1. F) + (- (- (0. F)))) * ((1. F) - (- (0. F)))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by A4, A5, RLVECT_1:def 11
.= (((1. F) + (- (- (0. F)))) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:def 11
.= (((1. F) + (0. F)) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= (((1. F) + (0. F)) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= ((1. F) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - ((0. F) * ((1. F) - (1. F))) by RLVECT_1:15
.= ((1. F) * (1. F)) - (0. F)
.= (1. F) - (0. F) ;
now :: thesis: for e9, f9, g9, h9 being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds
( not [[e9,f9],[g9,h9]] = [[a,b],[a,c]] or (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F )
let e9, f9, g9, h9 be Element of [: the carrier of F, the carrier of F, the carrier of F:]; :: thesis: ( not [[e9,f9],[g9,h9]] = [[a,b],[a,c]] or (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F )
assume A8: [[e9,f9],[g9,h9]] = [[a,b],[a,c]] ; :: thesis: ( (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F )
then A9: ( g9 = e & h9 = g ) by A6, MCART_1:93;
( e9 = e & f9 = f ) by A6, A8, MCART_1:93;
hence ( (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F ) by A7, A9, Lm2; :: thesis: verum
end;
hence not a,b '||' a,c by PARSP_1:12; :: thesis: verum