let p, q, r be Point of (TOP-REAL 3); :: thesis: for M being Matrix of 3,F_Real st M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> & the_rank_of M < 3 holds
ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
let M be Matrix of 3,F_Real; :: thesis: ( M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> & the_rank_of M < 3 implies ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) ) )
assume that
A1: M = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> and
A2: the_rank_of M < 3 ; :: thesis: ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
per cases ( lines M is linearly-dependent or not M is without_repeated_line ) by A2, Th31;
suppose A3: lines M is linearly-dependent ; :: thesis: ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
( Line (M,1) = p & Line (M,2) = q & Line (M,3) = r ) by A1, Th22;
then lines M = {p,q,r} by Th21;
then {p,q,r} is linearly-dependent by A3, MATRTOP2:7;
hence ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) ) by RLVECT_4:7; :: thesis: verum
end;
suppose not M is without_repeated_line ; :: thesis: ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) )
reconsider M2 = Mx2Tran M as linear-transformation of (RLSp2RVSp (TOP-REAL 3)),(RLSp2RVSp (TOP-REAL 3)) by Th33;
A4: not M2 is one-to-one by A2, MATRTOP1:39;
ex x being Element of (RLSp2RVSp (TOP-REAL 3)) st
( x in ker M2 & not x in (0). (RLSp2RVSp (TOP-REAL 3)) )
proof
assume A5: for x being Element of (RLSp2RVSp (TOP-REAL 3)) holds
( not x in ker M2 or x in (0). (RLSp2RVSp (TOP-REAL 3)) ) ; :: thesis: contradiction
A6: the carrier of (ker M2) c= the carrier of (RLSp2RVSp (TOP-REAL 3)) by VECTSP_4:def 2;
A7: the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) c= the carrier of (ker M2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) or x in the carrier of (ker M2) )
assume x in the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) ; :: thesis: x in the carrier of (ker M2)
then x in (0). (RLSp2RVSp (TOP-REAL 3)) ;
then x = 0. (RLSp2RVSp (TOP-REAL 3)) by VECTSP_4:35;
then x in ker M2 by RANKNULL:11;
hence x in the carrier of (ker M2) ; :: thesis: verum
end;
the carrier of (ker M2) c= the carrier of ((0). (RLSp2RVSp (TOP-REAL 3)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (ker M2) or x in the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) )
assume A8: x in the carrier of (ker M2) ; :: thesis: x in the carrier of ((0). (RLSp2RVSp (TOP-REAL 3)))
then A9: x in ker M2 ;
reconsider y = x as Element of the carrier of (RLSp2RVSp (TOP-REAL 3)) by A8, A6;
y in (0). (RLSp2RVSp (TOP-REAL 3)) by A5, A9;
hence x in the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) ; :: thesis: verum
end;
then the carrier of (ker M2) = the carrier of ((0). (RLSp2RVSp (TOP-REAL 3))) by A7;
hence contradiction by A4, MATRLIN2:43, VECTSP_4:29; :: thesis: verum
end;
then consider x2 being Element of (RLSp2RVSp (TOP-REAL 3)) such that
A10: x2 in ker M2 and
A11: not x2 in (0). (RLSp2RVSp (TOP-REAL 3)) ;
A12: x2 <> 0. (RLSp2RVSp (TOP-REAL 3)) by A11, VECTSP_4:35;
A13: RLSp2RVSp (TOP-REAL 3) = ModuleStr(# the carrier of (TOP-REAL 3), the addF of (TOP-REAL 3), the ZeroF of (TOP-REAL 3),(MultF_Real* (TOP-REAL 3)) #) by DUALSP01:def 2;
then A14: 0. (RLSp2RVSp (TOP-REAL 3)) = the ZeroF of (TOP-REAL 3) by STRUCT_0:def 6
.= 0. (TOP-REAL 3) by STRUCT_0:def 6 ;
then A15: (Mx2Tran M) . x2 = |[0,0,0]| by A10, EUCLID_5:4, RANKNULL:10;
reconsider pt = (Mx2Tran M) . x2 as Element of (TOP-REAL 3) by A10, A14, RANKNULL:10;
A16: <*(pt `1),(pt `2),(pt `3)*> = |[0,0,0]| by A15, EUCLID_5:3;
A17: pt `1 = pt . 1 by EUCLID_5:def 1;
RLSp2RVSp (TOP-REAL 3) = ModuleStr(# the carrier of (TOP-REAL 3), the addF of (TOP-REAL 3), the ZeroF of (TOP-REAL 3),(MultF_Real* (TOP-REAL 3)) #) by DUALSP01:def 2;
then the ZeroF of (RLSp2RVSp (TOP-REAL 3)) = 0. (TOP-REAL 3) by STRUCT_0:def 6;
then A18: x2 <> 0. (TOP-REAL 3) by A12, STRUCT_0:def 6;
A19: len M = 3 by MATRIX_0:def 2;
then A20: dom M = Seg 3 by FINSEQ_1:def 3;
then A21: ( len (Col (M,1)) = 3 & ( for j being Nat st j in Seg 3 holds
(Col (M,1)) . j = M * (j,1) ) ) by A19, MATRIX_0:def 8;
A22: ( (Col (M,1)) . 1 = M * (1,1) & (Col (M,1)) . 2 = M * (2,1) & (Col (M,1)) . 3 = M * (3,1) ) by A20, MATRIX_0:def 8, FINSEQ_1:1;
A23: ( len (Col (M,2)) = 3 & ( for j being Nat st j in Seg 3 holds
(Col (M,2)) . j = M * (j,2) ) ) by A19, A20, MATRIX_0:def 8;
A24: ( (Col (M,2)) . 1 = M * (1,2) & (Col (M,2)) . 2 = M * (2,2) & (Col (M,2)) . 3 = M * (3,2) ) by A20, MATRIX_0:def 8, FINSEQ_1:1;
A25: ( len (Col (M,3)) = 3 & ( for j being Nat st j in Seg 3 holds
(Col (M,3)) . j = M * (j,3) ) ) by A19, A20, MATRIX_0:def 8;
A26: ( (Col (M,3)) . 1 = M * (1,3) & (Col (M,3)) . 2 = M * (2,3) & (Col (M,3)) . 3 = M * (3,3) ) by A20, MATRIX_0:def 8, FINSEQ_1:1;
A27: pt `2 = pt . 2 by EUCLID_5:def 2;
reconsider x3 = x2 as Element of (TOP-REAL 3) by A13;
A28: pt `3 = pt . 3 by EUCLID_5:def 3;
reconsider x4 = x3 as FinSequence of F_Real by RVSUM_1:145;
A29: @ x3 = x3 by MATRTOP1:def 1;
then A30: @ x3 = <*(x3 `1),(x3 `2),(x3 `3)*> by EUCLID_5:3;
A31: 0 = pt . 1 by A17, A16, FINSEQ_1:78
.= (@ x3) "*" (Col (M,1)) by MATRTOP1:18 ;
reconsider a1 = x3 `1 , a2 = x3 `2 , a3 = x3 `3 , b1 = M * (1,1), b2 = M * (2,1), b3 = M * (3,1), c1 = M * (1,2), c2 = M * (2,2), c3 = M * (3,2), d1 = M * (1,3), d2 = M * (2,3), d3 = M * (3,3) as Element of F_Real by XREAL_0:def 1;
A32: <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> = <*<*(M * (1,1)),(M * (1,2)),(M * (1,3))*>,<*(M * (2,1)),(M * (2,2)),(M * (2,3))*>,<*(M * (3,1)),(M * (3,2)),(M * (3,3))*>*> by A1, MATRIXR2:37;
A33: p = <*(p `1),(p `2),(p `3)*> by EUCLID_5:3
.= <*(M * (1,1)),(M * (1,2)),(M * (1,3))*> by A32, FINSEQ_1:78 ;
A34: q = <*(q `1),(q `2),(q `3)*> by EUCLID_5:3
.= <*(M * (2,1)),(M * (2,2)),(M * (2,3))*> by A32, FINSEQ_1:78 ;
A35: r = <*(r `1),(r `2),(r `3)*> by EUCLID_5:3
.= <*(M * (3,1)),(M * (3,2)),(M * (3,3))*> by A32, FINSEQ_1:78 ;
reconsider q1 = <*(x3 `1),(x3 `2),(x3 `3)*>, r1 = <*(M * (1,1)),(M * (2,1)),(M * (3,1))*>, r2 = <*(M * (1,2)),(M * (2,2)),(M * (3,2))*>, r3 = <*(M * (1,3)),(M * (2,3)),(M * (3,3))*> as FinSequence of the carrier of F_Real by A29, EUCLID_5:3;
A36: 0 = q1 "*" r1 by A31, A22, A30, A21, FINSEQ_1:45
.= ((a1 * b1) + (a2 * b2)) + (a3 * b3) by Th6 ;
A37: 0 = pt . 2 by A16, FINSEQ_1:78, A27
.= (@ x3) "*" (Col (M,2)) by MATRTOP1:18 ;
A38: 0 = q1 "*" r2 by A37, A23, FINSEQ_1:45, A24, A30
.= ((a1 * c1) + (a2 * c2)) + (a3 * c3) by Th6 ;
A39: 0 = pt . 3 by A16, FINSEQ_1:78, A28
.= (@ x3) "*" (Col (M,3)) by MATRTOP1:18 ;
A40: 0 = q1 "*" r3 by A39, A26, A25, FINSEQ_1:45, A30
.= ((a1 * d1) + (a2 * d2)) + (a3 * d3) by Th6 ;
A41: ( a1 <> 0 or a2 <> 0 or a3 <> 0 ) by A18, EUCLID_5:3, EUCLID_5:4;
((a1 * p) + (a2 * q)) + (a3 * r) = (a1 * |[b1,c1,d1]|) + ((a2 * |[b2,c2,d2]|) + (a3 * |[b3,c3,d3]|)) by A33, RVSUM_1:15, A34, A35
.= (a1 * |[b1,c1,d1]|) + ((a2 * |[b2,c2,d2]|) + |[(a3 * b3),(a3 * c3),(a3 * d3)]|) by EUCLID_5:8
.= (a1 * |[b1,c1,d1]|) + (|[(a2 * b2),(a2 * c2),(a2 * d2)]| + |[(a3 * b3),(a3 * c3),(a3 * d3)]|) by EUCLID_5:8
.= |[(a1 * b1),(a1 * c1),(a1 * d1)]| + (|[(a2 * b2),(a2 * c2),(a2 * d2)]| + |[(a3 * b3),(a3 * c3),(a3 * d3)]|) by EUCLID_5:8
.= |[(a1 * b1),(a1 * c1),(a1 * d1)]| + |[((a2 * b2) + (a3 * b3)),((a2 * c2) + (a3 * c3)),((a2 * d2) + (a3 * d3))]| by EUCLID_5:6
.= |[((a1 * b1) + ((a2 * b2) + (a3 * b3))),((a1 * c1) + ((a2 * c2) + (a3 * c3))),((a1 * d1) + ((a2 * d2) + (a3 * d3)))]| by EUCLID_5:6
.= 0. (TOP-REAL 3) by A36, A38, A40, EUCLID_5:4 ;
hence ex a, b, c being Real st
( ((a * p) + (b * q)) + (c * r) = 0. (TOP-REAL 3) & ( a <> 0 or b <> 0 or c <> 0 ) ) by A41; :: thesis: verum
end;
end;