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:44;
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 3;
then ((K * ((e `1) - (f `1))) * ((e `2) - (g `2))) - ((K * ((e `2) - (f `2))) * ((e `1) - (g `1))) = 0. F by RLVECT_1:15;
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 3;
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 3;
then A6: K * ((((e `1) - (f `1)) * ((e `2) - (g `2))) - (((e `1) - (g `1)) * ((e `2) - (f `2)))) = 0. F by VECTSP_1:11;
( (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 3;
then ((K * ((e `1) - (f `1))) * ((e `3) - (g `3))) - ((K * ((e `3) - (f `3))) * ((e `1) - (g `1))) = 0. F by RLVECT_1:15;
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 3;
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 3;
then A7: K * ((((e `1) - (f `1)) * ((e `3) - (g `3))) - (((e `1) - (g `1)) * ((e `3) - (f `3)))) = 0. F by VECTSP_1:11;
( (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 3;
then ((K * ((e `2) - (f `2))) * ((e `3) - (g `3))) - ((K * ((e `3) - (f `3))) * ((e `2) - (g `2))) = 0. F by RLVECT_1:15;
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 3;
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 3;
then A8: K * ((((e `2) - (f `2)) * ((e `3) - (g `3))) - (((e `2) - (g `2)) * ((e `3) - (f `3)))) = 0. F by VECTSP_1:11;
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:12;
then A10: K = 0. F by A6, A8, A7, VECTSP_1:12;
then A11: 0. F = L * ((e `3) - (g `3)) by A4, VECTSP_1:7;
( 0. F = L * ((e `1) - (g `1)) & 0. F = L * ((e `2) - (g `2)) ) by A2, A3, A10, VECTSP_1:7;
hence ( K = 0. F & L = 0. F ) by A6, A8, A7, A9, A11, A5, VECTSP_1:12; :: thesis: verum