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 )

hereby :: thesis: ( Det M <> 0. K implies M is invertible )

assume M is invertible ; :: thesis: Det M <> 0. K
then Det M is unital by Th34;
then Det M divides 1. K by GCD_1:def 20;
then consider y being Element of K such that
A1: 1. K = (Det M) * y by GCD_1:def 1;
Det M <> 0. K

proof

assume Det M = 0. K ; :: thesis: contradiction
then 1. K = (0. K) * y by A1;
hence contradiction ; :: thesis: verum

end;

hence Det M <> 0. K ; :: thesis: verum

end;

assume Det M <> 0. K ; :: thesis: M is invertible
then (Det M) * ((Det M) ") = 1. K by VECTSP_1:def 10;
then Det M divides 1. K by GCD_1:def 1;
hence M is invertible by Th34, GCD_1:def 20; :: thesis: verum