let n be Nat; :: thesis: for M being Matrix of n,REAL holds
( M is invertible iff MXR2MXF M is invertible )
let M be Matrix of n,REAL; :: thesis: ( M is invertible iff MXR2MXF M is invertible )
hereby :: thesis: ( MXR2MXF M is invertible implies M is invertible )
assume M is invertible ; :: thesis: MXR2MXF M is invertible
then consider B being Matrix of n,REAL such that
A1: ( B * M = 1_Rmatrix n & M * B = 1_Rmatrix n ) by MATRIXR2:def 5;
thus MXR2MXF M is invertible by A1, MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum
end;
assume MXR2MXF M is invertible ; :: thesis: M is invertible
then consider M2 being Matrix of n,F_Real such that
A2: MXR2MXF M is_reverse_of M2 by MATRIX_6:def 3;
set B = MXF2MXR M2;
A3: M * (MXF2MXR M2) = 1_Rmatrix n by A2, MATRIX_6:def 2;
(MXF2MXR M2) * M = 1_Rmatrix n by A2, MATRIX_6:def 2;
hence M is invertible by A3, MATRIXR2:def 5; :: thesis: verum