let ra be non zero Real; :: thesis: for N, O, M being Matrix of 3,3,REAL st N is invertible & M = ra * O & M = ((N @) * O) * N holds
(((Inv N) @) * O) * (Inv N) = (1 / ra) * O
let N, O, M be Matrix of 3,3,REAL; :: thesis: ( N is invertible & M = ra * O & M = ((N @) * O) * N implies (((Inv N) @) * O) * (Inv N) = (1 / ra) * O )
assume that
A1: N is invertible and
A3: M = ra * O and
A4: M = ((N @) * O) * N ; :: thesis: (((Inv N) @) * O) * (Inv N) = (1 / ra) * O
reconsider NI = Inv N, NIT = (Inv N) @ as Matrix of 3,3,REAL ;
A5: ( (Inv N) @ = Inv (N @) & N @ is invertible ) by A1, Th52;
A6: ( len NI = 3 & width NI = 3 & width (O * N) = 3 & len (O * N) = 3 ) by MATRIX_0:24;
reconsider ira = 1 / ra as Real ;
reconsider NTON = ((N @) * O) * N as Matrix of REAL ;
A7: len NTON = 3 by MATRIX_0:24;
A8: width (NI @) = 3 by MATRIX_0:24;
O = 1 * O by MATRIXR1:32
.= ((1 / ra) * ra) * O by XCMPLX_1:87
.= ira * (((N @) * O) * N) by A3, A4, MATRIXR2:11 ;
then ((NI @) * O) * NI = (ira * ((NI @) * (((N @) * O) * N))) * NI by A8, A7, MATRIXR1:40
.= (ira * (NIT * ((N @) * (O * N)))) * NI by MATRIXR2:27
.= (ira * ((NIT * (N @)) * (O * N))) * NI by MATRIXR2:27
.= (ira * ((1_Rmatrix 3) * (O * N))) * NI by A5, MATRIXR2:def 6
.= (ira * (O * N)) * NI by MATRIXR2:70
.= ira * ((O * N) * NI) by A6, MATRIXR1:41
.= ira * (O * (N * NI)) by MATRIXR2:27
.= ira * (O * (1_Rmatrix 3)) by A1, MATRIXR2:def 6
.= ira * O by MATRIXR2:71 ;
hence (((Inv N) @) * O) * (Inv N) = (1 / ra) * O ; :: thesis: verum