let N be invertible Matrix of 3,F_Real; :: thesis: for NR, M, M2 being Matrix of 3,REAL st NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) holds
((NR @) * M2) * NR = M
let NR, M, M2 be Matrix of 3,REAL; :: thesis: ( NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) implies ((NR @) * M2) * NR = M )
assume that
A1: NR = MXF2MXR N and
A2: M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) ; :: thesis: ((NR @) * M2) * NR = M
reconsider NI = MXF2MXR ((MXR2MXF NR) ~), NJ = MXF2MXR ((MXR2MXF (NR @)) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
A3: NI * NR = 1_Rmatrix 3 by A1, Lm10;
((NR @) * M2) * NR = (((NR @) * NJ) * M) * (NI * NR) by A2, Lm04
.= ((1_Rmatrix 3) * M) * (1_Rmatrix 3) by A1, Lm09, A3
.= M * (1_Rmatrix 3) by MATRIXR2:70
.= M by MATRIXR2:71 ;
hence ((NR @) * M2) * NR = M ; :: thesis: verum