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

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