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_0:24;

A2: width (M1 @) = n by MATRIX_0:24;

A3: len (M1 ~) = n by MATRIX_0:24;

A4: width (M1 ~) = n by MATRIX_0:24;

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) ) )

then A9: M1 ~ is_reverse_of M1 by Def4;

(M1 @) * M1 = (M1 ~) * M1 by A8;

hence ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) by A9; :: thesis: verum

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_0:24;

A2: width (M1 @) = n by MATRIX_0:24;

A3: len (M1 ~) = n by MATRIX_0:24;

A4: width (M1 ~) = n by MATRIX_0:24;

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 A8:
M1 is Orthogonal
; :: thesis: ( M1 is invertible & (M1 @) * M1 = 1. (K,n) )
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;

then (M1 ~) * (M1 * (M1 ~)) = ((M1 @) * M1) * (M1 ~) by A1, A4, A3, MATRIX_3:33;

then (M1 ~) * (M1 * (M1 ~)) = (M1 @) * (M1 * (M1 ~)) by A1, A3, A2, MATRIX_3:33;

then (M1 ~) * (1. (K,n)) = (M1 @) * (M1 * (M1 ~)) by A7;

then (M1 ~) * (1. (K,n)) = (M1 @) * (1. (K,n)) by A7;

then M1 ~ = (M1 @) * (1. (K,n)) by MATRIX_3:19;

then M1 ~ = M1 @ by MATRIX_3:19;

hence M1 is Orthogonal by A5; :: thesis: verum

end;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;

then (M1 ~) * (M1 * (M1 ~)) = ((M1 @) * M1) * (M1 ~) by A1, A4, A3, MATRIX_3:33;

then (M1 ~) * (M1 * (M1 ~)) = (M1 @) * (M1 * (M1 ~)) by A1, A3, A2, MATRIX_3:33;

then (M1 ~) * (1. (K,n)) = (M1 @) * (M1 * (M1 ~)) by A7;

then (M1 ~) * (1. (K,n)) = (M1 @) * (1. (K,n)) by A7;

then M1 ~ = (M1 @) * (1. (K,n)) by MATRIX_3:19;

then M1 ~ = M1 @ by MATRIX_3:19;

hence M1 is Orthogonal by A5; :: thesis: verum

then A9: M1 ~ is_reverse_of M1 by Def4;

(M1 @) * M1 = (M1 ~) * M1 by A8;

hence ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) by A9; :: thesis: verum