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