let n be Nat; for K being Field
for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal
let K be Field; for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal
let M1, M2 be Matrix of n,K; ( n > 0 & M1 is Orthogonal & M2 is Orthogonal implies (M1 ~) * M2 is Orthogonal )
assume that
A1:
n > 0
and
A2:
M1 is Orthogonal
and
A3:
M2 is Orthogonal
; (M1 ~) * M2 is Orthogonal
A4:
M1 is invertible
by A2;
then A5:
M1 ~ is invertible
;
A6:
M2 is invertible
by A3;
then A7:
(M1 ~) * M2 is invertible
by A5, Th36;
((M1 ~) * M2) ~ = (M2 ~) * ((M1 ~) ~)
by A6, A5, Th36;
then A8:
((M1 ~) * M2) ~ = (M2 ~) * M1
by A4, Th16;
A9:
len M2 = n
by MATRIX_0:24;
A10:
( width (M1 ~) = n & width M2 = n )
by MATRIX_0:24;
A11:
( width M1 = n & len M1 = n )
by MATRIX_0:24;
( M1 @ = M1 ~ & M2 @ = M2 ~ )
by A2, A3;
then ((M1 ~) * M2) @ =
(M2 ~) * ((M1 @) @)
by A1, A10, A9, MATRIX_3:22
.=
(M2 ~) * M1
by A1, A11, MATRIX_0:57
;
hence
(M1 ~) * M2 is Orthogonal
by A7, A8; verum