let i, j, n be Nat; 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; 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; ( 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
; (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
; verum