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