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

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum