let F be Field; :: thesis: for a, b, c, p, q, r being Element of (MPS F) st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r
let a, b, c, p, q, r be Element of (MPS F); :: thesis: ( not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r )
assume that
A1: not a,p '||' a,b and
A2: not a,p '||' a,c and
A3: a,p '||' b,q and
A4: a,p '||' c,r and
A5: a,b '||' p,q and
A6: a,c '||' p,r ; :: thesis: b,c '||' q,r
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A7: [[a,p],[c,r]] = [[i,j],[k,l]] and
( ex L being Element of F st
( L * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & L * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & L * ((i `3_3) - (j `3_3)) = (k `3_3) - (l `3_3) ) or ( (i `1_3) - (j `1_3) = 0. F & (i `2_3) - (j `2_3) = 0. F & (i `3_3) - (j `3_3) = 0. F ) ) by A4, Th2;
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A8: [[a,b],[p,q]] = [[e,f],[g,h]] and
( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A5, Th2;
A9: ( a = e & p = g ) by A8, MCART_1:93;
A10: c = k by A7, MCART_1:93;
then A11: [[a,p],[c,r]] = [[e,g],[k,l]] by A9, A7, MCART_1:93;
then A12: l `1_3 = ((g `1_3) + (k `1_3)) - (e `1_3) by A2, A4, A6, Th5;
A13: b = f by A8, MCART_1:93;
then A14: [[a,p],[b,q]] = [[e,g],[f,h]] by A8, A9, MCART_1:93;
then h `1_3 = ((g `1_3) + (f `1_3)) - (e `1_3) by A1, A3, A5, Th5;
then A15: (1_ F) * ((f `1_3) - (k `1_3)) = (h `1_3) - (l `1_3) by A12, Lm10;
A16: l `3_3 = ((g `3_3) + (k `3_3)) - (e `3_3) by A2, A4, A6, A11, Th5;
A17: l `2_3 = ((g `2_3) + (k `2_3)) - (e `2_3) by A2, A4, A6, A11, Th5;
h `3_3 = ((g `3_3) + (f `3_3)) - (e `3_3) by A1, A3, A5, A14, Th5;
then A18: (1_ F) * ((f `3_3) - (k `3_3)) = (h `3_3) - (l `3_3) by A16, Lm10;
h `2_3 = ((g `2_3) + (f `2_3)) - (e `2_3) by A1, A3, A5, A14, Th5;
then A19: (1_ F) * ((f `2_3) - (k `2_3)) = (h `2_3) - (l `2_3) by A17, Lm10;
q = h by A8, MCART_1:93;
then [[b,c],[q,r]] = [[f,k],[h,l]] by A13, A7, A10, MCART_1:93;
hence b,c '||' q,r by A15, A19, A18, Th2; :: thesis: verum