let F be Field; :: thesis: for a, b, c, d being Element of (MPS F)
for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [[a,b],[c,d]] = [[e,f],[g,h]] holds
( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
let a, b, c, d be Element of (MPS F); :: thesis: for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [[a,b],[c,d]] = [[e,f],[g,h]] holds
( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
let e, f, g, h be Element of [: the carrier of F, the carrier of F, the carrier of F:]; :: thesis: ( not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [[a,b],[c,d]] = [[e,f],[g,h]] implies ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) ) )
assume that
A1: not a,b '||' a,c and
A2: a,b '||' c,d and
A3: a,c '||' b,d and
A4: [[a,b],[c,d]] = [[e,f],[g,h]] ; :: thesis: ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
consider m, n, o, w being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A6: [[a,c],[b,d]] = [[m,n],[o,w]] and
A7: ( ex L being Element of F st
( L * ((m `1_3) - (n `1_3)) = (o `1_3) - (w `1_3) & L * ((m `2_3) - (n `2_3)) = (o `2_3) - (w `2_3) & L * ((m `3_3) - (n `3_3)) = (o `3_3) - (w `3_3) ) or ( (m `1_3) - (n `1_3) = 0. F & (m `2_3) - (n `2_3) = 0. F & (m `3_3) - (n `3_3) = 0. F ) ) by A3, Th2;
A8: b = f by A4, MCART_1:93;
then A9: o = f by A6, MCART_1:93;
d = h by A4, MCART_1:93;
then A10: w = h by A6, MCART_1:93;
c = g by A4, MCART_1:93;
then A11: n = g by A6, MCART_1:93;
A12: a = e by A4, MCART_1:93;
then A13: [[a,b],[a,c]] = [[e,f],[e,g]] by A4, A8, MCART_1:93;
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A14: [[a,b],[c,d]] = [[i,j],[k,l]] and
A15: ( ex K being Element of F st
( K * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & K * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & K * ((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 A2, Th2;
A16: ( e = i & f = j ) by A4, A14, MCART_1:93;
A17: ( g = k & h = l ) by A4, A14, MCART_1:93;
A18: e = m by A12, A6, MCART_1:93;
f = [(f `1_3),(f `2_3),(f `3_3)] ;
then ( e `1_3 <> f `1_3 or e `2_3 <> f `2_3 or e `3_3 <> f `3_3 ) by A1, A13, Th3;
then consider K being Element of F such that
A19: K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) and
A20: K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) and
A21: K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) by A15, A16, A17, Lm2;
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, A13, Th3;
then consider L being Element of F such that
A22: L * ((e `1_3) - (g `1_3)) = (f `1_3) - (h `1_3) and
A23: L * ((e `2_3) - (g `2_3)) = (f `2_3) - (h `2_3) and
A24: L * ((e `3_3) - (g `3_3)) = (f `3_3) - (h `3_3) by A7, A18, A11, A9, A10, Lm2;
(K * ((e `2_3) - (f `2_3))) - (L * ((e `2_3) - (g `2_3))) = (g `2_3) - (f `2_3) by A20, A23, Lm5;
then A25: (K + (- (1_ F))) * ((e `2_3) - (f `2_3)) = (L + (- (1_ F))) * ((e `2_3) - (g `2_3)) by Lm6;
(K * ((e `3_3) - (f `3_3))) - (L * ((e `3_3) - (g `3_3))) = (g `3_3) - (f `3_3) by A21, A24, Lm5;
then A26: (K + (- (1_ F))) * ((e `3_3) - (f `3_3)) = (L + (- (1_ F))) * ((e `3_3) - (g `3_3)) by Lm6;
(K * ((e `1_3) - (f `1_3))) - (L * ((e `1_3) - (g `1_3))) = (g `1_3) - (f `1_3) by A19, A22, Lm5;
then (K + (- (1_ F))) * ((e `1_3) - (f `1_3)) = (L + (- (1_ F))) * ((e `1_3) - (g `1_3)) by Lm6;
then A27: K + (- (1_ F)) = 0. F by A1, A13, A25, A26, Th4;
then ((e `2_3) - (f `2_3)) * (1_ F) = (g `2_3) - (h `2_3) by A20, Lm2;
then A28: (e `2_3) - (f `2_3) = (g `2_3) - (h `2_3) ;
((e `3_3) - (f `3_3)) * (1_ F) = (g `3_3) - (h `3_3) by A21, A27, Lm2;
then A29: (e `3_3) - (f `3_3) = (g `3_3) - (h `3_3) ;
((e `1_3) - (f `1_3)) * (1_ F) = (g `1_3) - (h `1_3) by A19, A27, Lm2;
then (e `1_3) - (f `1_3) = (g `1_3) - (h `1_3) ;
hence ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) ) by A28, A29, Lm7; :: thesis: verum