let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st M1 is Orthogonal holds
M2 * M1 is_congruent_Matrix_of M1 * M2
let K be Field; for M1, M2 being Matrix of n,K st M1 is Orthogonal holds
M2 * M1 is_congruent_Matrix_of M1 * M2
let M1, M2 be Matrix of n,K; ( M1 is Orthogonal implies M2 * M1 is_congruent_Matrix_of M1 * M2 )
A1:
( len M2 = n & width (M1 ~) = n )
by MATRIX_0:24;
assume A2:
M1 is Orthogonal
; M2 * M1 is_congruent_Matrix_of M1 * M2
then
M1 is invertible
by MATRIX_6:def 7;
then A3:
M1 ~ is_reverse_of M1
by MATRIX_6:def 4;
take
M1
; MATRIX_8:def 6 ( M1 is invertible & M2 * M1 = ((M1 @) * (M1 * M2)) * M1 )
( len M1 = n & width M1 = n )
by MATRIX_0:24;
then ((M1 ~) * (M1 * M2)) * M1 =
(((M1 ~) * M1) * M2) * M1
by A1, MATRIX_3:33
.=
((1. (K,n)) * M2) * M1
by A3, MATRIX_6:def 2
.=
M2 * M1
by MATRIX_3:18
;
hence
( M1 is invertible & M2 * M1 = ((M1 @) * (M1 * M2)) * M1 )
by A2, MATRIX_6:def 7; verum