let n be Nat; :: thesis: for K being Field

for M being Matrix of n,K st M is invertible holds

( M @ is invertible & (M @) ~ = (M ~) @ )

let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds

( M @ is invertible & (M @) ~ = (M ~) @ )

let M be Matrix of n,K; :: thesis: ( M is invertible implies ( M @ is invertible & (M @) ~ = (M ~) @ ) )

assume A1: M is invertible ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )

set M1 = M @ ;

set M2 = (M ~) @ ;

for M being Matrix of n,K st M is invertible holds

( M @ is invertible & (M @) ~ = (M ~) @ )

let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds

( M @ is invertible & (M @) ~ = (M ~) @ )

let M be Matrix of n,K; :: thesis: ( M is invertible implies ( M @ is invertible & (M @) ~ = (M ~) @ ) )

assume A1: M is invertible ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )

set M1 = M @ ;

set M2 = (M ~) @ ;

per cases
( n > 0 or n = 0 )
by NAT_1:3;

end;

suppose A2:
n > 0
; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )

A3:
( width M = n & width (M ~) = n )
by MATRIX_0:24;

len M = n by MATRIX_0:24;

then A4: ((M ~) * M) @ = (M @) * ((M ~) @) by A2, A3, MATRIX_3:22;

A5: M ~ is_reverse_of M by A1, Def4;

then A6: (M @) * ((M ~) @) = 1. (K,n) by A4, Th10;

len (M ~) = n by MATRIX_0:24;

then (M * (M ~)) @ = ((M ~) @) * (M @) by A2, A3, MATRIX_3:22;

then (M @) * ((M ~) @) = ((M ~) @) * (M @) by A5, A4;

then A7: M @ is_reverse_of (M ~) @ by A6;

then M @ is invertible ;

hence ( M @ is invertible & (M @) ~ = (M ~) @ ) by A7, Def4; :: thesis: verum

end;len M = n by MATRIX_0:24;

then A4: ((M ~) * M) @ = (M @) * ((M ~) @) by A2, A3, MATRIX_3:22;

A5: M ~ is_reverse_of M by A1, Def4;

then A6: (M @) * ((M ~) @) = 1. (K,n) by A4, Th10;

len (M ~) = n by MATRIX_0:24;

then (M * (M ~)) @ = ((M ~) @) * (M @) by A2, A3, MATRIX_3:22;

then (M @) * ((M ~) @) = ((M ~) @) * (M @) by A5, A4;

then A7: M @ is_reverse_of (M ~) @ by A6;

then M @ is invertible ;

hence ( M @ is invertible & (M @) ~ = (M ~) @ ) by A7, Def4; :: thesis: verum