let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum