let ra be Real; for O, M being Matrix of 3,REAL st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )
let O, M be Matrix of 3,REAL; ( O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O implies ( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) ) )
assume that
A1:
O = symmetric_3 (1,1,(- 1),0,0,0)
and
A2:
M = ra * O
; ( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )
1_Rmatrix 3 = MXF2MXR (1. (F_Real,3))
by MATRIXR2:def 2;
then A3:
MXR2MXF (1_Rmatrix 3) = 1. (F_Real,3)
by ANPROJ_8:16;
A4: O * O =
(symmetric_3 (1,1,(- 1),0,0,0)) * (symmetric_3 (1,1,(- 1),0,0,0))
by A1, ANPROJ_8:17
.=
1_Rmatrix 3
by Th43, A3, MATRIXR1:def 1
;
( len O = 3 & width O = 3 )
by MATRIX_0:23;
hence
( O * M = ra * (1_Rmatrix 3) & M * O = ra * (1_Rmatrix 3) )
by A4, A2, MATRIXR1:40, MATRIXR1:41; verum