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 A2: N >= 1 ; :: thesis: Det M <> 0. K
A3: M * M1 = 1. (K,n) by ;
Det (1. (K,n)) = 1_ K by ;
then (Det M) * (Det M1) = 1_ K by ;
hence Det M <> 0. K ; :: thesis: verum
end;
end;
end;
set C = ((Det M) ") * ();
assume A4: Det M <> 0. K ; :: thesis: M is invertible
then A5: M * (((Det M) ") * ()) = 1. (K,n) by Th30;
(((Det M) ") * ()) * M = 1. (K,n) by ;
then M is_reverse_of ((Det M) ") * () by ;
hence M is invertible by MATRIX_6:def 3; :: thesis: verum