let F be Field; :: thesis: for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b
let a, b, p, q, r, s be Element of (MPS F); :: thesis: ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b )
defpred S1[ Element of H1(F), Element of H1(F), Element of H1(F), Element of H1(F)] means ( ((($1 `1) - ($2 `1)) * (($3 `2) - ($4 `2))) - ((($3 `1) - ($4 `1)) * (($1 `2) - ($2 `2))) = 0. F & ((($1 `1) - ($2 `1)) * (($3 `3) - ($4 `3))) - ((($3 `1) - ($4 `1)) * (($1 `3) - ($2 `3))) = 0. F & ((($1 `2) - ($2 `2)) * (($3 `3) - ($4 `3))) - ((($3 `2) - ($4 `2)) * (($1 `3) - ($2 `3))) = 0. F );
assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s ; :: thesis: ( p,q '||' r,s or a = b )
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A3: [e,f,g,h] = [a,b,p,q] and
A4: S1[e,f,g,h] by A1, Th23;
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A5: [i,j,k,l] = [a,b,r,s] and
A6: S1[i,j,k,l] by A2, Th23;
A7: ( i = a & j = b ) by A5, MCART_1:29;
A8: ( k = r & l = s ) by A5, MCART_1:29;
set A = (e `1) - (f `1);
set B = (e `2) - (f `2);
set C = (e `3) - (f `3);
set D = (g `1) - (h `1);
set E = (g `2) - (h `2);
set K = (g `3) - (h `3);
set G = (k `1) - (l `1);
set H = (k `2) - (l `2);
set I = (k `3) - (l `3);
A9: ( e = a & f = b ) by A3, MCART_1:29;
A10: ( g = p & h = q ) by A3, MCART_1:29;
now
assume A11: a <> b ; :: thesis: ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [g,h,k,l] = [p,q,r,s] & S1[g,h,k,l] )
now
e = [(e `1),(e `2),(e `3)] by MCART_1:44;
then A12: ( e `1 <> f `1 or e `2 <> f `2 or e `3 <> f `3 ) by A9, A11, MCART_1:44;
per cases ( (e `1) - (f `1) <> 0. F or (e `2) - (f `2) <> 0. F or (e `3) - (f `3) <> 0. F ) by A12, RLVECT_1:21;
case A13: (e `1) - (f `1) <> 0. F ; :: thesis: ( (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F & (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F & (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F )
hence (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F by A4, A6, A9, A7, Lm4; :: thesis: ( (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F & (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F )
thus A14: (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F by A4, A6, A9, A7, A13, Lm4; :: thesis: (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F
( ((g `2) - (h `2)) * ((k `3) - (l `3)) = ((((g `1) - (h `1)) * ((e `2) - (f `2))) * (((e `1) - (f `1)) ")) * ((k `3) - (l `3)) & ((k `2) - (l `2)) * ((g `3) - (h `3)) = ((((k `1) - (l `1)) * ((e `2) - (f `2))) * (((e `1) - (f `1)) ")) * ((g `3) - (h `3)) ) by A4, A6, A9, A7, A13, VECTSP_1:30;
hence (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F by A14, Lm8; :: thesis: verum
end;
case A15: (e `2) - (f `2) <> 0. F ; :: thesis: ( (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F & (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F & (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F )
hence (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis: ( (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F & (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F )
thus A16: (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F by A4, A6, A9, A7, A15, Lm4; :: thesis: (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F
( ((g `1) - (h `1)) * ((k `3) - (l `3)) = ((((g `2) - (h `2)) * ((e `1) - (f `1))) * (((e `2) - (f `2)) ")) * ((k `3) - (l `3)) & ((k `1) - (l `1)) * ((g `3) - (h `3)) = ((((k `2) - (l `2)) * ((e `1) - (f `1))) * (((e `2) - (f `2)) ")) * ((g `3) - (h `3)) ) by A4, A6, A9, A7, A15, VECTSP_1:30;
hence (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F by A16, Lm8; :: thesis: verum
end;
case A17: (e `3) - (f `3) <> 0. F ; :: thesis: ( (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F & (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F & (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F )
hence (((g `2) - (h `2)) * ((k `3) - (l `3))) - (((k `2) - (l `2)) * ((g `3) - (h `3))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis: ( (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F & (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F )
A18: ( ((g `1) - (h `1)) * ((k `2) - (l `2)) = ((((g `3) - (h `3)) * ((e `1) - (f `1))) * (((e `3) - (f `3)) ")) * ((k `2) - (l `2)) & ((k `1) - (l `1)) * ((g `2) - (h `2)) = ((((k `3) - (l `3)) * ((e `1) - (f `1))) * (((e `3) - (f `3)) ")) * ((g `2) - (h `2)) ) by A4, A6, A9, A7, A17, VECTSP_1:30;
(((g `3) - (h `3)) * ((k `2) - (l `2))) - (((k `3) - (l `3)) * ((g `2) - (h `2))) = 0. F by A4, A6, A9, A7, A17, Lm6;
hence (((g `1) - (h `1)) * ((k `2) - (l `2))) - (((k `1) - (l `1)) * ((g `2) - (h `2))) = 0. F by A18, Lm8; :: thesis: (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F
thus (((g `1) - (h `1)) * ((k `3) - (l `3))) - (((k `1) - (l `1)) * ((g `3) - (h `3))) = 0. F by A4, A6, A9, A7, A17, Lm6; :: thesis: verum
end;
end;
end;
hence ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [g,h,k,l] = [p,q,r,s] & S1[g,h,k,l] ) by A10, A8; :: thesis: verum
end;
hence ( p,q '||' r,s or a = b ) by Th23; :: thesis: verum