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

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;
reconsider N = n as Element of NAT by ORDINAL1:def 13;

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

then ( Det (1. K,n) = 1_ K & M * M1 = 1. K,n ) by A1, MATRIX_6:def 2, MATRIX_7:16;
then ( (Det M) * (Det M1) = 1_ K & 1_ K <> 0. K ) by A2, MATRIX11:62;
hence Det M <> 0. K by VECTSP_1:44; :: thesis: verum

end;

end;

end;

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