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 ~) @ ;
per cases ( n > 0 or n = 0 ) by NAT_1:3;
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;
suppose n = 0 ; :: thesis: ( M @ is invertible & (M @) ~ = (M ~) @ )
then B1: M = 1. (K,n) by MATRIX_0:45;
then B2: M @ = 1. (K,n) by Th10;
then (M @) ~ = 1. (K,n) by Th8;
hence ( M @ is invertible & (M @) ~ = (M ~) @ ) by B1, B2; :: thesis: verum
end;
end;