let n be Nat; :: thesis: for K being Ring
for M1 being Matrix of n,K holds
( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )
let K be Ring; :: thesis: for M1 being Matrix of n,K holds
( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )
let M1 be Matrix of n,K; :: thesis: ( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal )
A1: ( width M1 = n & len M1 = n ) by MATRIX_0:24;
A2: len (M1 @) = n by MATRIX_0:24;
A3: width (M1 ~) = n by MATRIX_0:24;
A4: len (M1 ~) = n by MATRIX_0:24;
thus ( M1 * (M1 @) = 1. (K,n) & M1 is invertible implies M1 is Orthogonal ) :: thesis: ( M1 is Orthogonal implies ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) )

proof

assume that
A5: M1 * (M1 @) = 1. (K,n) and
A6: M1 is invertible ; :: thesis: M1 is Orthogonal
A7: M1 ~ is_reverse_of M1 by A6, Def4;
then (M1 ~) * (M1 * (M1 ~)) = (M1 ~) * (M1 * (M1 @)) by A5;
then ((M1 ~) * M1) * (M1 ~) = (M1 ~) * (M1 * (M1 @)) by A1, A3, A4, MATRIX_3:33;
then ((M1 ~) * M1) * (M1 ~) = ((M1 ~) * M1) * (M1 @) by A1, A3, A2, MATRIX_3:33;
then (1. (K,n)) * (M1 ~) = ((M1 ~) * M1) * (M1 @) by A7;
then (1. (K,n)) * (M1 ~) = (1. (K,n)) * (M1 @) by A7;
then M1 ~ = (1. (K,n)) * (M1 @) by MATRIX_3:18;
then M1 ~ = M1 @ by MATRIX_3:18;
hence M1 is Orthogonal by A6; :: thesis: verum

end;

assume A8: M1 is Orthogonal ; :: thesis: ( M1 * (M1 @) = 1. (K,n) & M1 is invertible )
then A9: M1 ~ is_reverse_of M1 by Def4;
M1 * (M1 @) = M1 * (M1 ~) by A8;
hence ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) by A9; :: thesis: verum