let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n)
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
(((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n)
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies (((Det M) ") * ((Matrix_of_Cofactor M) @)) * 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 CM = (((Det M) ") * ((Matrix_of_Cofactor M) @)) * M;
set ID = 1. (K,n);
assume A1: Det M <> 0. K ; :: thesis: (((Det M) ") * ((Matrix_of_Cofactor M) @)) * M = 1. (K,n)

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

A2: Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * 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 ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) implies (1. (K,n)) * (b₁,b₂) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b₁,b₂) )
assume A3: [i,j] in Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) ; :: thesis: (1. (K,n)) * (b₁,b₂) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b₁,b₂)
reconsider COL = Col (M,j), L = Line (((Matrix_of_Cofactor 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 M = n by MATRIX_0:24;
A5: Indices ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A6: i in Seg n by A3, ZFMISC_1:87;
then A7: 1 <= i by FINSEQ_1:1;
A8: j in Seg n by A3, A5, ZFMISC_1:87;
len ((Matrix_of_Cofactor M) @) = n by MATRIX_0:24;
then i <= len ((Matrix_of_Cofactor M) @) by A6, FINSEQ_1:1;
then Line ((((Det M) ") * ((Matrix_of_Cofactor M) @)),i) = ((Det M) ") * L by A7, MATRIXR1:20;
then mlt ((Line ((((Det M) ") * ((Matrix_of_Cofactor M) @)),i)),(Col (M,j))) = ((Det M) ") * (mlt (L,COL)) by FVSUM_1:69;
then A9: (Line ((((Det M) ") * ((Matrix_of_Cofactor M) @)),i)) "*" (Col (M,j)) = ((Det M) ") * ((Line (((Matrix_of_Cofactor M) @),i)) "*" (Col (M,j))) by FVSUM_1:73
.= ((Det M) ") * (Det (RLine ((M @),i9,(Line ((M @),j9))))) by A6, A8, Th32 ;
A10: width (((Det M) ") * ((Matrix_of_Cofactor M) @)) = n by MATRIX_0:24;
then A11: ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (i,j) = ((Det M) ") * (Det (RLine ((M @),i,(Line ((M @),j))))) 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₂) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (b₁,b₂)

then A13: RLine ((M @),i,(Line ((M @),j))) = M @ by MATRIX11:30;
A14: Det M = Det (M @) by MATRIXR2:43;
A15: ((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) = ((((Det M) ") * ((Matrix_of_Cofactor M) @)) * M) * (i,j) by A3, A10, A4, A9, A13, A15, A14, MATRIX_3:def 4; :: thesis: verum

end;

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

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

end;

end;

end;

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