let n be Nat; :: thesis: for K being domRing
for M being Matrix of n,K holds
( M is invertible iff Det M is unital )
let K be domRing; :: thesis: for M being Matrix of n,K holds
( M is invertible iff Det M is unital )
let M be Matrix of n,K; :: thesis: ( M is invertible iff Det M is unital )
thus ( M is invertible implies Det M is unital ) :: thesis: ( Det M is unital implies M is invertible )

proof

reconsider N = n as Element of NAT by ORDINAL1:def 12;
assume M is invertible ; :: thesis: Det M is unital
then consider M1 being Matrix of n,K such that
A1: M is_reverse_of M1 by MATRIX_6:def 3;

per cases ( N = 0 or N >= 1 ) by NAT_1:14;

suppose N = 0 ; :: thesis: Det M is unital

then Det M = 1_ K by MATRIXR2:41
.= 1. K ;
hence Det M is unital ; :: thesis: verum

end;

suppose A2: N >= 1 ; :: thesis: Det M is unital

A3: M * M1 = 1. (K,n) by A1, MATRIX_6:def 2;
Det (1. (K,n)) = 1_ K by A2, MATRIX_7:16;
then (Det M) * (Det M1) = 1_ K by A2, A3, MATRIX11:62
.= 1. K ;
hence Det M is unital by GCD_1:def 1, GCD_1:def 20; :: thesis: verum

end;

end;

end;

set C = ((Det M) ") * ((Matrix_of_Cofactor M) @);
assume A4: Det M is unital ; :: thesis: M is invertible
then A5: M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) by Th30;
(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n) by A4, Th33;
then M is_reverse_of ((Det M) ") * ((Matrix_of_Cofactor M) @) by A5, MATRIX_6:def 2;
hence M is invertible by MATRIX_6:def 3; :: thesis: verum