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 )

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

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

set C = ((Det M) ") * ((Matrix_of_Cofactor M) @);
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;

end;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;

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