let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K holds
( M is invertible iff Det M <> 0. K )
let K be Field; :: thesis: for M being Matrix of n,K holds
( M is invertible iff Det M <> 0. K )
let M be Matrix of n,K; :: thesis: ( M is invertible iff Det M <> 0. K )
thus ( M is invertible implies Det M <> 0. K ) :: thesis: ( Det M <> 0. K implies M is invertible )

proof

reconsider N = n as Element of NAT by ORDINAL1:def 12;
assume M is invertible ; :: thesis: Det M <> 0. K
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 <> 0. K

then Det M = 1_ K by MATRIXR2:41;
hence Det M <> 0. K ; :: thesis: verum

end;

suppose A2: N >= 1 ; :: thesis: Det M <> 0. K

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;
hence Det M <> 0. K ; :: thesis: verum

end;

end;

end;

set C = ((Det M) ") * ((Matrix_of_Cofactor M) @);
assume A4: Det M <> 0. K ; :: 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