let F be Field; :: thesis: for a, b, c being Element of (MPS F)
for e, f, g being Element of [:the carrier of F,the carrier of F,the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) holds
( K = 0. F & L = 0. F )
let a, b, c be Element of (MPS F); :: thesis: for e, f, g being Element of [:the carrier of F,the carrier of F,the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) holds
( K = 0. F & L = 0. F )
let e, f, g be Element of [:the carrier of F,the carrier of F,the carrier of F:]; :: thesis: for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) holds
( K = 0. F & L = 0. F )
let K, L be Element of F; :: thesis: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) implies ( K = 0. F & L = 0. F ) )
assume that
A1: not a,b '||' a,c and
A2: [a,b,a,c] = [e,f,e,g] and
A3: ( K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) ) ; :: thesis: ( K = 0. F & L = 0. F )
( (K * ((e `1 ) - (f `1 ))) * ((e `2 ) - (g `2 )) = L * (((e `1 ) - (g `1 )) * ((e `2 ) - (g `2 ))) & (K * ((e `2 ) - (f `2 ))) * ((e `1 ) - (g `1 )) = L * (((e `2 ) - (g `2 )) * ((e `1 ) - (g `1 ))) & (K * ((e `2 ) - (f `2 ))) * ((e `3 ) - (g `3 )) = L * (((e `2 ) - (g `2 )) * ((e `3 ) - (g `3 ))) & (K * ((e `3 ) - (f `3 ))) * ((e `2 ) - (g `2 )) = L * (((e `3 ) - (g `3 )) * ((e `2 ) - (g `2 ))) & (K * ((e `1 ) - (f `1 ))) * ((e `3 ) - (g `3 )) = L * (((e `1 ) - (g `1 )) * ((e `3 ) - (g `3 ))) & (K * ((e `3 ) - (f `3 ))) * ((e `1 ) - (g `1 )) = L * (((e `3 ) - (g `3 )) * ((e `1 ) - (g `1 ))) ) by A3, GROUP_1:def 4;
then ( ((K * ((e `1 ) - (f `1 ))) * ((e `2 ) - (g `2 ))) - ((K * ((e `2 ) - (f `2 ))) * ((e `1 ) - (g `1 ))) = 0. F & ((K * ((e `2 ) - (f `2 ))) * ((e `3 ) - (g `3 ))) - ((K * ((e `3 ) - (f `3 ))) * ((e `2 ) - (g `2 ))) = 0. F & ((K * ((e `1 ) - (f `1 ))) * ((e `3 ) - (g `3 ))) - ((K * ((e `3 ) - (f `3 ))) * ((e `1 ) - (g `1 ))) = 0. F ) by RLVECT_1:28;
then ( (K * (((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 )))) - ((K * ((e `2 ) - (f `2 ))) * ((e `1 ) - (g `1 ))) = 0. F & (K * (((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 )))) - ((K * ((e `3 ) - (f `3 ))) * ((e `2 ) - (g `2 ))) = 0. F & (K * (((e `1 ) - (f `1 )) * ((e `3 ) - (g `3 )))) - ((K * ((e `3 ) - (f `3 ))) * ((e `1 ) - (g `1 ))) = 0. F ) by GROUP_1:def 4;
then ( (K * (((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 )))) - (K * (((e `2 ) - (f `2 )) * ((e `1 ) - (g `1 )))) = 0. F & (K * (((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 )))) - (K * (((e `3 ) - (f `3 )) * ((e `2 ) - (g `2 )))) = 0. F & (K * (((e `1 ) - (f `1 )) * ((e `3 ) - (g `3 )))) - (K * (((e `3 ) - (f `3 )) * ((e `1 ) - (g `1 )))) = 0. F ) by GROUP_1:def 4;
then A4: ( K * ((((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 ))) - (((e `1 ) - (g `1 )) * ((e `2 ) - (f `2 )))) = 0. F & K * ((((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 ))) - (((e `2 ) - (g `2 )) * ((e `3 ) - (f `3 )))) = 0. F & K * ((((e `1 ) - (f `1 )) * ((e `3 ) - (g `3 ))) - (((e `1 ) - (g `1 )) * ((e `3 ) - (f `3 )))) = 0. F ) by VECTSP_1:43;
A5: ( (((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 ))) - (((e `1 ) - (g `1 )) * ((e `2 ) - (f `2 ))) <> 0. F or (((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 ))) - (((e `2 ) - (g `2 )) * ((e `3 ) - (f `3 ))) <> 0. F or (((e `1 ) - (f `1 )) * ((e `3 ) - (g `3 ))) - (((e `1 ) - (g `1 )) * ((e `3 ) - (f `3 ))) <> 0. F ) by A1, A2, PARSP_1:23;
then K = 0. F by A4, VECTSP_1:44;
then A6: ( 0. F = L * ((e `1 ) - (g `1 )) & 0. F = L * ((e `2 ) - (g `2 )) & 0. F = L * ((e `3 ) - (g `3 )) ) by A3, VECTSP_1:39;
( e = [(e `1 ),(e `2 ),(e `3 )] & g = [(g `1 ),(g `2 ),(g `3 )] ) by MCART_1:48;
then ( e `1 <> g `1 or e `2 <> g `2 or e `3 <> g `3 ) by A1, A2, Th3;
then ( (e `1 ) - (g `1 ) <> 0. F or (e `2 ) - (g `2 ) <> 0. F or (e `3 ) - (g `3 ) <> 0. F ) by Lm2;
hence ( K = 0. F & L = 0. F ) by A4, A5, A6, VECTSP_1:44; :: thesis: verum