let i, j, n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st i in Seg n holds
(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))
let K be Field; :: thesis: for M being Matrix of n,K st i in Seg n holds
(Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))
let M be Matrix of n,K; :: thesis: ( i in Seg n implies (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j)))) )
assume A1: i in Seg n ; :: thesis: (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) = Det (RLine (M,i,(Line (M,j))))
set C = Matrix_of_Cofactor M;
len (Matrix_of_Cofactor M) = n by MATRIX_0:24;
then dom (Matrix_of_Cofactor M) = Seg n by FINSEQ_1:def 3;
then A2: Line ((Matrix_of_Cofactor M),i) = Col (((Matrix_of_Cofactor M) @),i) by A1, MATRIX_0:58;
width M = n by MATRIX_0:24;
then A3: len (Line (M,j)) = n by MATRIX_0:def 7;
thus Det (RLine (M,i,(Line (M,j)))) = Sum (LaplaceExpL ((RLine (M,i,(Line (M,j)))),i)) by A1, Th25
.= Sum (mlt ((Col (((Matrix_of_Cofactor M) @),i)),(Line (M,j)))) by A1, A2, A3, Th28
.= (Line (M,j)) "*" (Col (((Matrix_of_Cofactor M) @),i)) by FVSUM_1:64 ; :: thesis: verum