let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st M is invertible holds
for i, j being Nat st [i,j] in Indices (M ~ ) holds
(M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i)
let K be Field; :: thesis: for M being Matrix of n,K st M is invertible holds
for i, j being Nat st [i,j] in Indices (M ~ ) holds
(M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i)
let M be Matrix of n,K; :: thesis: ( M is invertible implies for i, j being Nat st [i,j] in Indices (M ~ ) holds
(M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i) )
assume A1: M is invertible ; :: thesis: for i, j being Nat st [i,j] in Indices (M ~ ) holds
(M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i)
let i, j be Nat; :: thesis: ( [i,j] in Indices (M ~ ) implies (M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i) )
assume A2: [i,j] in Indices (M ~ ) ; :: thesis: (M ~ ) * i,j = (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i)
set COF = Matrix_of_Cofactor M;
set D = Det M;
A3: [i,j] in Indices ((Matrix_of_Cofactor M) @ ) by A2, MATRIX_1:27;
then A4: [j,i] in Indices (Matrix_of_Cofactor M) by MATRIX_1:def 7;
Det M <> 0. K by A1, Th34;
hence (M ~ ) * i,j = (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * i,j by Th35
.= ((Det M) " ) * (((Matrix_of_Cofactor M) @ ) * i,j) by A3, MATRIX_3:def 5
.= ((Det M) " ) * ((Matrix_of_Cofactor M) * j,i) by A4, MATRIX_1:def 7
.= ((Det M) " ) * (Cofactor M,j,i) by A4, Def6
.= (((Det M) " ) * ((power K) . (- (1_ K)),(i + j))) * (Minor M,j,i) by GROUP_1:def 4 ;
:: thesis: verum