Metamath Proof Explorer

Theorem maducoevalmin1

Description: The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018)

		Ref	Expression
	Hypotheses	maducoevalmin1.a	$⊢ A = N Mat R$
		maducoevalmin1.b	$⊢ B = {Base}_{A}$
		maducoevalmin1.d	$⊢ D = N maDet R$
		maducoevalmin1.j	$⊢ J = N maAdju R$
	Assertion	maducoevalmin1	$⊢ (M \in B \land I \in N \land H \in N) \to I J (M) H = D (H (N minMatR1 R) (M) I)$

Proof

Step	Hyp	Ref	Expression
1		maducoevalmin1.a	$⊢ A = N Mat R$
2		maducoevalmin1.b	$⊢ B = {Base}_{A}$
3		maducoevalmin1.d	$⊢ D = N maDet R$
4		maducoevalmin1.j	$⊢ J = N maAdju R$
5		eqid	$⊢ 1_{R} = 1_{R}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	1 3 4 2 5 6	maducoeval	$⊢ (M \in B \land I \in N \land H \in N) \to I J (M) H = D ((i \in N, j \in N ⟼ if (i = H, if (j = I, 1_{R}, 0_{R}), i M j)))$
8		eqid	$⊢ N minMatR1 R = N minMatR1 R$
9	1 2 8 5 6	minmar1val	$⊢ (M \in B \land H \in N \land I \in N) \to H (N minMatR1 R) (M) I = (i \in N, j \in N ⟼ if (i = H, if (j = I, 1_{R}, 0_{R}), i M j))$
10	9	3com23	$⊢ (M \in B \land I \in N \land H \in N) \to H (N minMatR1 R) (M) I = (i \in N, j \in N ⟼ if (i = H, if (j = I, 1_{R}, 0_{R}), i M j))$
11	10	eqcomd	$⊢ (M \in B \land I \in N \land H \in N) \to (i \in N, j \in N ⟼ if (i = H, if (j = I, 1_{R}, 0_{R}), i M j)) = H (N minMatR1 R) (M) I$
12	11	fveq2d	$⊢ (M \in B \land I \in N \land H \in N) \to D ((i \in N, j \in N ⟼ if (i = H, if (j = I, 1_{R}, 0_{R}), i M j))) = D (H (N minMatR1 R) (M) I)$
13	7 12	eqtrd	$⊢ (M \in B \land I \in N \land H \in N) \to I J (M) H = D (H (N minMatR1 R) (M) I)$