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 & [a,b,a,c] = [e,f,e,g] ) and
A2: K * ((e `1 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) and
A3: K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) and
A4: K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) ; :: thesis: ( K = 0. F & L = 0. F )
( 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, Th3;
then A5: ( (e `1 ) - (g `1 ) <> 0. F or (e `2 ) - (g `2 ) <> 0. F or (e `3 ) - (g `3 ) <> 0. F ) by Lm2;
( (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 ))) ) by A2, 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 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 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 by GROUP_1:def 4;
then A6: K * ((((e `1 ) - (f `1 )) * ((e `2 ) - (g `2 ))) - (((e `1 ) - (g `1 )) * ((e `2 ) - (f `2 )))) = 0. F by VECTSP_1:43;
( (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 A2, A4, GROUP_1:def 4;
then ((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 `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 `3 ) - (g `3 )))) - (K * (((e `3 ) - (f `3 )) * ((e `1 ) - (g `1 )))) = 0. F by GROUP_1:def 4;
then A7: K * ((((e `1 ) - (f `1 )) * ((e `3 ) - (g `3 ))) - (((e `1 ) - (g `1 )) * ((e `3 ) - (f `3 )))) = 0. F by VECTSP_1:43;
( (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 ))) ) by A3, A4, GROUP_1:def 4;
then ((K * ((e `2 ) - (f `2 ))) * ((e `3 ) - (g `3 ))) - ((K * ((e `3 ) - (f `3 ))) * ((e `2 ) - (g `2 ))) = 0. F by RLVECT_1:28;
then (K * (((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 )))) - ((K * ((e `3 ) - (f `3 ))) * ((e `2 ) - (g `2 ))) = 0. F by GROUP_1:def 4;
then (K * (((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 )))) - (K * (((e `3 ) - (f `3 )) * ((e `2 ) - (g `2 )))) = 0. F by GROUP_1:def 4;
then A8: K * ((((e `2 ) - (f `2 )) * ((e `3 ) - (g `3 ))) - (((e `2 ) - (g `2 )) * ((e `3 ) - (f `3 )))) = 0. F by VECTSP_1:43;
A9: ( (((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, PARSP_1:23;
then A10: K = 0. F by A6, A8, A7, VECTSP_1:44;
then A11: 0. F = L * ((e `3 ) - (g `3 )) by A4, VECTSP_1:39;
( 0. F = L * ((e `1 ) - (g `1 )) & 0. F = L * ((e `2 ) - (g `2 )) ) by A2, A3, A10, VECTSP_1:39;
hence ( K = 0. F & L = 0. F ) by A6, A8, A7, A9, A11, A5, VECTSP_1:44; :: thesis: verum