let F be Field; 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); ( 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
; 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; verum