let n be Nat; :: thesis: for N being Matrix of n,F_Real
for M being Matrix of n,REAL st M is invertible & N = MXR2MXF M holds
N is invertible
let N be Matrix of n,F_Real; :: thesis: for M being Matrix of n,REAL st M is invertible & N = MXR2MXF M holds
N is invertible
let M be Matrix of n,REAL; :: thesis: ( M is invertible & N = MXR2MXF M implies N is invertible )
assume that
A1: M is invertible and
A2: N = MXR2MXF M ; :: thesis: N is invertible
consider MI being Matrix of n,REAL such that
A3: MI * M = 1_Rmatrix n and
A4: M * MI = 1_Rmatrix n by A1;
reconsider NI = MXR2MXF MI as Matrix of n,F_Real ;
now :: thesis: ( N * NI = NI * N & N * NI = 1. (F_Real,n) )
A5: N * NI = MXR2MXF (M * MI) by A2, Lm07
.= 1. (F_Real,n) by A4, ANPROJ_8:16 ;
A6: NI * N = MXR2MXF (MI * M) by A2, Lm07
.= 1. (F_Real,n) by A3, ANPROJ_8:16 ;
thus N * NI = NI * N by A5, A6; :: thesis: N * NI = 1. (F_Real,n)
thus N * NI = 1. (F_Real,n) by A5; :: thesis: verum
end;
hence N is invertible by MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum