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, Def7;
then A5: M1 ~ is invertible by Th16;
A6: M2 is invertible by A3, Def7;
then A7: (M1 ~) * M2 is invertible by A5, Th37;
((M1 ~) * M2) ~ = (M2 ~) * ((M1 ~) ~) by A6, A5, Th37;
then A8: ((M1 ~) * M2) ~ = (M2 ~) * M1 by A4, Th16;
A9: len M2 = n by MATRIX_1:25;
A10: ( width (M1 ~) = n & width M2 = n ) by MATRIX_1:25;
A11: ( width M1 = n & len M1 = n ) by MATRIX_1:25;
( M1 @ = M1 ~ & M2 @ = M2 ~ ) by A2, A3, Def7;
then ((M1 ~) * M2) @ = (M2 ~) * ((M1 @) @) by A1, A10, A9, MATRIX_3:24
.= (M2 ~) * M1 by A1, A11, MATRIX_2:15 ;
hence (M1 ~) * M2 is Orthogonal by A7, A8, Def7; :: thesis: verum