let N be invertible Matrix of 3,F_Real; :: thesis: for NR, M1, M2 being Matrix of 3,REAL
for a, b, c, d, e, f being Real st NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) holds
MXR2MXF M2 is symmetric
let NR, M1, M2 be Matrix of 3,REAL; :: thesis: for a, b, c, d, e, f being Real st NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) holds
MXR2MXF M2 is symmetric
let a, b, c, d, e, f be Real; :: thesis: ( NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) implies MXR2MXF M2 is symmetric )
assume A1: ( NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) ) ; :: thesis: MXR2MXF M2 is symmetric
reconsider M = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) as Matrix of 3,REAL ;
A2: MXR2MXF M = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) by MATRIXR1:def 1;
reconsider Q = (MXR2MXF (NR @)) ~ as Matrix of 3,F_Real ;
reconsider T = MXF2MXR ((MXR2MXF (NR @)) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
T * M is Matrix of 3,REAL ;
then reconsider M3 = (MXF2MXR ((MXR2MXF (NR @)) ~)) * M, M4 = MXF2MXR ((MXR2MXF NR) ~) as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M5 = (MXR2MXF (NR @)) ~ as Matrix of 3,F_Real ;
reconsider M6 = MXF2MXR M5 as Matrix of 3,REAL by MATRIXR1:def 2;
NR @ is invertible by A1, Lm12;
then A3: MXR2MXF (NR @) is invertible by Lm15;
A4: (MXR2MXF (NR @)) @ = MXR2MXF NR
proof
reconsider N1 = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
A5: NR @ = N @ by A1, MATRIXR1:def 2;
reconsider N2 = MXR2MXF (NR @) as Matrix of 3,F_Real ;
A6: ( len N = 3 & width N = 3 ) by MATRIX_0:24;
(MXR2MXF (NR @)) @ = (N @) @ by A5, MATRIXR1:def 1
.= N by A6, MATRIX_0:57 ;
hence (MXR2MXF (NR @)) @ = MXR2MXF NR by A1, ANPROJ_8:16; :: thesis: verum
end;
A7: M5 @ = (MXR2MXF NR) ~ by A3, MATRIX14:31, A4;
MXR2MXF M2 is symmetric
proof
A8: ( len M5 = 3 & width M5 = 3 ) by MATRIX_0:24;
MXR2MXF M2 = (MXR2MXF M3) * (MXR2MXF M4) by A1, Lm07
.= (MXR2MXF (M6 * M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~)))
.= ((MXR2MXF (MXF2MXR M5)) * (MXR2MXF M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~))) by Lm07
.= (M5 * (MXR2MXF M)) * (MXR2MXF (MXF2MXR ((MXR2MXF NR) ~))) by ANPROJ_8:16
.= (M5 * (MXR2MXF M)) * ((MXR2MXF NR) ~) by ANPROJ_8:16
.= (((M5 @) @) * (MXR2MXF M)) * (M5 @) by A7, A8, MATRIX_0:57 ;
hence MXR2MXF M2 is symmetric by A2, Th12, Th07; :: thesis: verum
end;
hence MXR2MXF M2 is symmetric ; :: thesis: verum