let n be Nat; :: thesis: for R being commutative Ring
for M1, M2 being Matrix of n,R st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal
let R be commutative Ring; :: thesis: for M1, M2 being Matrix of n,R st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds
(M1 ~) * M2 is Orthogonal
let M1, M2 be Matrix of n,R; :: 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, Th37;
((M1 ~) * M2) ~ = (M2 ~) * ((M1 ~) ~) by A6, A5, Th37;
then A8: ((M1 ~) * M2) ~ = (M2 ~) * M1 by A4, Th17;
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