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