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

proof

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

end;

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