let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n)
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n)
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) )
set D = Det M;
set D9 = (Det M) " ;
set C = Matrix_of_Cofactor M;
set DC = ((Det M) ") * ((Matrix_of_Cofactor M) @);
set MC = M * (((Det M) ") * ((Matrix_of_Cofactor M) @));
set ID = 1. (K,n);
assume A1: Det M <> 0. K ; :: thesis: M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n)

now :: thesis: for i, j being Nat st [i,j] in Indices (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) holds
(1. (K,n)) * (i,j) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (i,j)

A2: Indices (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) = Indices (1. (K,n)) by MATRIX_0:26;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
let i, j be Nat; :: thesis: ( [i,j] in Indices (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) implies (1. (K,n)) * (b₁,b₂) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (b₁,b₂) )
assume A3: [i,j] in Indices (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) ; :: thesis: (1. (K,n)) * (b₁,b₂) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (b₁,b₂)
reconsider COL = Col (((Matrix_of_Cofactor M) @),j), L = Line (M,i) as Element of N -tuples_on the carrier of K by MATRIX_0:24;
reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;
A4: len (((Det M) ") * ((Matrix_of_Cofactor M) @)) = n by MATRIX_0:24;
A5: Indices (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A6: i in Seg n by A3, ZFMISC_1:87;
A7: j in Seg n by A3, A5, ZFMISC_1:87;
then A8: 1 <= j by FINSEQ_1:1;
width ((Matrix_of_Cofactor M) @) = n by MATRIX_0:24;
then j <= width ((Matrix_of_Cofactor M) @) by A7, FINSEQ_1:1;
then Col ((((Det M) ") * ((Matrix_of_Cofactor M) @)),j) = ((Det M) ") * COL by A8, MATRIXR1:19;
then mlt ((Line (M,i)),(Col ((((Det M) ") * ((Matrix_of_Cofactor M) @)),j))) = ((Det M) ") * (mlt (L,COL)) by FVSUM_1:69;
then A9: (Line (M,i)) "*" (Col ((((Det M) ") * ((Matrix_of_Cofactor M) @)),j)) = ((Det M) ") * ((Line (M,i)) "*" (Col (((Matrix_of_Cofactor M) @),j))) by FVSUM_1:73
.= ((Det M) ") * (Det (RLine (M,j9,(Line (M,i9))))) by A7, Th29 ;
A10: width M = n by MATRIX_0:24;
then A11: (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (i,j) = ((Det M) ") * (Det (RLine (M,j,(Line (M,i))))) by A3, A4, A9, MATRIX_3:def 4;

per cases ( i = j or i <> j ) ;

suppose A12: i = j ; :: thesis: (1. (K,n)) * (b₁,b₂) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (b₁,b₂)

then A13: RLine (M,j,(Line (M,i))) = M by MATRIX11:30;
A14: (Det M) * ((Det M) ") = 1_ K by A1, VECTSP_1:def 10;
(1. (K,n)) * (i,j) = 1_ K by A3, A2, A12, MATRIX_1:def 3;
hence (1. (K,n)) * (i,j) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (i,j) by A3, A10, A4, A9, A13, A14, MATRIX_3:def 4; :: thesis: verum

end;

suppose A15: i <> j ; :: thesis: (1. (K,n)) * (b₁,b₂) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (b₁,b₂)

then A16: (1. (K,n)) * (i,j) = 0. K by A3, A2, MATRIX_1:def 3;
Det (RLine (M,j9,(Line (M,i9)))) = 0. K by A6, A7, A15, MATRIX11:51;
hence (1. (K,n)) * (i,j) = (M * (((Det M) ") * ((Matrix_of_Cofactor M) @))) * (i,j) by A11, A16; :: thesis: verum

end;

end;

end;

hence M * (((Det M) ") * ((Matrix_of_Cofactor M) @)) = 1. (K,n) by MATRIX_0:27; :: thesis: verum