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
((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O
let O, M be Matrix of 3,REAL; ( O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O implies ((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O )
assume that
A1:
O = symmetric_3 (1,1,(- 1),0,0,0)
and
A2:
M = ra * O
; ((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O
reconsider O1 = O as Matrix of 3,F_Real ;
A3:
O @ = O
by A1, PASCAL:12, MATRIX_6:def 5;
reconsider MR = M as Matrix of 3,F_Real ;
A4:
MR is symmetric
by Th54, A2, A1, PASCAL:12;
A5:
((ra * (1_Rmatrix 3)) * O) * (ra * (1_Rmatrix 3)) = (ra ^2) * O
proof
reconsider z1 = 1,
z2 =
- 1,
z3 =
0 as
Element of
F_Real by XREAL_0:def 1;
A6:
O = <*<*z1,z3,z3*>,<*z3,z1,z3*>,<*z3,z3,z2*>*>
by A1, PASCAL:def 3;
reconsider ea =
ra as
Element of
F_Real by XREAL_0:def 1;
A7:
ra * (1_Rmatrix 3) =
MXF2MXR (ea * (MXR2MXF (1_Rmatrix 3)))
by MATRIXR1:def 7
.=
MXF2MXR (ea * (MXR2MXF (MXF2MXR (1. (F_Real,3)))))
by MATRIXR2:def 2
.=
MXF2MXR (ea * (1. (F_Real,3)))
by ANPROJ_8:16
.=
ea * (1. (F_Real,3))
by MATRIXR1:def 2
.=
<*<*(ea * z1),(ea * z3),(ea * z3)*>,<*(ea * z3),(ea * z1),(ea * z3)*>,<*(ea * z3),(ea * z3),(ea * z1)*>*>
by ANPROJ_9:1, Th39
.=
<*<*ea,z3,z3*>,<*z3,ea,z3*>,<*z3,z3,ea*>*>
;
then reconsider RA1R =
ra * (1_Rmatrix 3) as
Matrix of 3,
F_Real by ANPROJ_8:19;
reconsider ea2 =
ra * ra as
Element of
F_Real by XREAL_0:def 1;
reconsider z4 =
ea * z2 as
Element of
F_Real ;
A8:
RA1R * O1 =
<*<*(((ea * z1) + (z3 * z3)) + (z3 * z3)),(((ea * z3) + (z3 * z1)) + (z3 * z3)),(((ea * z3) + (z3 * z3)) + (z3 * z2))*>,<*(((z3 * z1) + (ea * z3)) + (z3 * z3)),(((z3 * z3) + (ea * z1)) + (z3 * z3)),(((z3 * z3) + (ea * z3)) + (z3 * z2))*>,<*(((z3 * z1) + (z3 * z3)) + (ea * z3)),(((z3 * z3) + (z3 * z1)) + (ea * z3)),(((z3 * z3) + (z3 * z3)) + (ea * z2))*>*>
by A7, A6, ANPROJ_9:6
.=
<*<*ea,z3,z3*>,<*z3,ea,z3*>,<*z3,z3,z4*>*>
;
A9:
(RA1R * O1) * RA1R =
<*<*(((ea * ea) + (z3 * z3)) + (z3 * z3)),(((ea * z3) + (z3 * ea)) + (z3 * z3)),(((ea * z3) + (z3 * z3)) + (z3 * ea))*>,<*(((z3 * ea) + (ea * z3)) + (z3 * z3)),(((z3 * z3) + (ea * ea)) + (z3 * z3)),(((z3 * z3) + (ea * z3)) + (z3 * ea))*>,<*(((z3 * ea) + (z3 * z3)) + (z4 * z3)),(((z3 * z3) + (z3 * ea)) + (z4 * z3)),(((z3 * z3) + (z3 * z3)) + (z4 * ea))*>*>
by A8, A7, ANPROJ_9:6
.=
<*<*(ea * ea),z3,z3*>,<*z3,(ea * ea),z3*>,<*z3,z3,(z4 * ea)*>*>
;
A10:
(ra * (1_Rmatrix 3)) * O = RA1R * O1
by ANPROJ_8:17;
(ra ^2) * O =
MXF2MXR (ea2 * (MXR2MXF O))
by MATRIXR1:def 7
.=
ea2 * (MXR2MXF O)
by MATRIXR1:def 2
.=
<*<*(ea2 * z1),(ea2 * z3),(ea2 * z3)*>,<*(ea2 * z3),(ea2 * z1),(ea2 * z3)*>,<*(ea2 * z3),(ea2 * z3),(ea2 * z2)*>*>
by A6, Th39, MATRIXR1:def 1
;
hence
((ra * (1_Rmatrix 3)) * O) * (ra * (1_Rmatrix 3)) = (ra ^2) * O
by A10, A9, ANPROJ_8:17;
verum
end;
((((M @) * O) @) * O) * ((M @) * O) =
(((M * O) @) * O) * ((M @) * O)
by A4, MATRIX_6:def 5
.=
(((M * O) @) * O) * (M * O)
by A4, MATRIX_6:def 5
.=
(((O @) * (M @)) * O) * (M * O)
by MATRIXR2:30
.=
((O * M) * O) * (M * O)
by A3, A4, MATRIX_6:def 5
.=
((ra * (1_Rmatrix 3)) * O) * (M * O)
by A1, A2, Th55
.=
(ra ^2) * O
by A1, A2, A5, Th55
;
hence
((((M @) * O) @) * O) * ((M @) * O) = (ra ^2) * O
; verum