let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds
M1 @ commutes_with M2
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds
M1 @ commutes_with M2
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is Orthogonal & M1 commutes_with M2 implies M1 @ commutes_with M2 )
set M3 = M1 @ ;
assume A1: ( M1 is Orthogonal & M1 commutes_with M2 ) ; :: thesis: M1 @ commutes_with M2
then ( M1 is invertible & M1 @ = M1 ~ ) by Def7;
then A2: M1 ~ is_reverse_of M1 by Def4;
A3: ( width M1 = n & len M2 = n & width M2 = n & len M1 = n & width (M1 ~ ) = n & len (M1 ~ ) = n ) by MATRIX_1:25;
A4: ( width ((M1 ~ ) * M2) = n & len ((M1 ~ ) * M2) = n ) by MATRIX_1:25;
M2 * (M1 @ ) = ((1. K,n) * M2) * (M1 @ ) by MATRIX_3:20
.= (((M1 ~ ) * M1) * M2) * (M1 @ ) by A2, Def2
.= ((M1 ~ ) * (M1 * M2)) * (M1 @ ) by A3, MATRIX_3:35
.= ((M1 ~ ) * (M2 * M1)) * (M1 @ ) by A1, Def1
.= ((M1 ~ ) * (M2 * M1)) * (M1 ~ ) by A1, Def7
.= (((M1 ~ ) * M2) * M1) * (M1 ~ ) by A3, MATRIX_3:35
.= ((M1 ~ ) * M2) * (M1 * (M1 ~ )) by A3, A4, MATRIX_3:35
.= ((M1 ~ ) * M2) * (1. K,n) by A2, Def2
.= (M1 ~ ) * M2 by MATRIX_3:21
.= (M1 @ ) * M2 by A1, Def7 ;
hence M1 @ commutes_with M2 by Def1; :: thesis: verum