let p, q, r be Point of (TOP-REAL 3); :: thesis: for M being Matrix of 3,F_Real
for pm, qm, rm being Point of (TOP-REAL 3)
for pt, qt, rt being FinSequence of 1 -tuples_on REAL
for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
let M be Matrix of 3,F_Real; :: thesis: for pm, qm, rm being Point of (TOP-REAL 3)
for pt, qt, rt being FinSequence of 1 -tuples_on REAL
for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
let pm, qm, rm be Point of (TOP-REAL 3); :: thesis: for pt, qt, rt being FinSequence of 1 -tuples_on REAL
for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
let pt, qt, rt be FinSequence of 1 -tuples_on REAL; :: thesis: for pf, qf, rf being FinSequence of F_Real st M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm holds
( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
let pf, qf, rf be FinSequence of F_Real; :: thesis: ( M is invertible & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf & M2F pt = pm & M2F qt = qm & M2F rt = rm implies ( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 ) )
assume that
A1: M is invertible and
A2: p = pf and
A3: q = qf and
A4: r = rf and
A5: pt = M * pf and
A6: qt = M * qf and
A7: rt = M * rf and
A8: M2F pt = pm and
A9: M2F qt = qm and
A10: M2F rt = rm ; :: thesis: ( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 )
reconsider PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> as Matrix of 3,F_Real by Th16;
A11: Det M <> 0. F_Real by A1, LAPLACE:34;
A12: ( pm = <*(pm `1),(pm `2),(pm `3)*> & qm = <*(qm `1),(qm `2),(qm `3)*> & rm = <*(rm `1),(rm `2),(rm `3)*> ) by EUCLID_5:3;
( p = <*(p `1),(p `2),(p `3)*> & q = <*(q `1),(q `2),(q `3)*> & r = <*(r `1),(r `2),(r `3)*> ) by EUCLID_5:3;
then PQR @ = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> by Th20;
then A13: (M * (PQR @)) @ = <*pm,qm,rm*> by A8, A9, A10, A2, A3, A4, A5, A6, A7, Th77;
A14: Det ((M * (PQR @)) @) = Det (M * (PQR @)) by MATRIXR2:43
.= (Det M) * (Det (PQR @)) by MATRIXR2:45
.= (Det M) * (Det PQR) by MATRIXR2:43 ;
( Det PQR = 0. F_Real iff Det ((M * (PQR @)) @) = 0. F_Real )
proof
thus ( Det PQR = 0. F_Real implies Det ((M * (PQR @)) @) = 0. F_Real ) by A14; :: thesis: ( Det ((M * (PQR @)) @) = 0. F_Real implies Det PQR = 0. F_Real )
assume Det ((M * (PQR @)) @) = 0. F_Real ; :: thesis: Det PQR = 0. F_Real
then ((Det M) ") * ((Det M) * (Det PQR)) = (Det M) * (0. F_Real) by A14;
then (((Det M) ") * (Det M)) * (Det PQR) = 0. F_Real ;
then (1. F_Real) * (Det PQR) = 0. F_Real by A11, VECTSP_1:def 10;
hence Det PQR = 0. F_Real ; :: thesis: verum
end;
then ( |{p,q,r}| = 0. F_Real iff |{pm,qm,rm}| = 0. F_Real ) by A13, A12, Th29;
hence ( |{p,q,r}| = 0 iff |{pm,qm,rm}| = 0 ) by STRUCT_0:def 6; :: thesis: verum