let ra be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum