smadiadetg

Description: The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. (Contributed by AV, 14-Feb-2019)

	Ref	Expression
Hypotheses	smadiadet.a	$⊢ A = N Mat R$
	smadiadet.b	$⊢ B = {Base}_{A}$
	smadiadet.r	$⊢ R \in CRing$
	smadiadet.d	$⊢ D = N maDet R$
	smadiadet.h	$⊢ E = (N ∖ \{K\}) maDet R$
	smadiadetg.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	smadiadetg	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to D (K (M (N matRRep R) S) K) = S \underset{˙}{\cdot} E (K (N subMat R) (M) K)$

Proof

Step	Hyp	Ref	Expression
1		smadiadet.a	$⊢ A = N Mat R$
2		smadiadet.b	$⊢ B = {Base}_{A}$
3		smadiadet.r	$⊢ R \in CRing$
4		smadiadet.d	$⊢ D = N maDet R$
5		smadiadet.h	$⊢ E = (N ∖ \{K\}) maDet R$
6		smadiadetg.x	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	3	a1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to R \in CRing$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	3 9	mp1i	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to R \in Ring$
11		simp1	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to M \in B$
12		simp3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to S \in {Base}_{R}$
13		simp2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K \in N$
14	1 2	marrepcl	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land K \in N)) \to K (M (N matRRep R) S) K \in B$
15	10 11 12 13 13 14	syl32anc	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (M (N matRRep R) S) K \in B$
16	1 2	minmar1cl	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land K \in N)) \to K (N minMatR1 R) (M) K \in B$
17	10 11 13 13 16	syl22anc	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to K (N minMatR1 R) (M) K \in B$
18	1 2 3 4 5 6	smadiadetglem2	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{(\{K\} \times N)} = ((\{K\} \times N) \times \{S\}) {\underset{˙}{\cdot}}_{f} ({(K (N minMatR1 R) (M) K) ↾}_{(\{K\} \times N)})$
19	1 2 3 4 5	smadiadetglem1	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to {(K (M (N matRRep R) S) K) ↾}_{((N ∖ \{K\}) \times N)} = {(K (N minMatR1 R) (M) K) ↾}_{((N ∖ \{K\}) \times N)}$
20	4 1 2 7 6 8 15 12 17 13 18 19	mdetrsca	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to D (K (M (N matRRep R) S) K) = S \underset{˙}{\cdot} D (K (N minMatR1 R) (M) K)$
21	1 2 3 4 5	smadiadet	$⊢ (M \in B \land K \in N) \to E (K (N subMat R) (M) K) = D (K (N minMatR1 R) (M) K)$
22	21	3adant3	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to E (K (N subMat R) (M) K) = D (K (N minMatR1 R) (M) K)$
23	22	eqcomd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to D (K (N minMatR1 R) (M) K) = E (K (N subMat R) (M) K)$
24	23	oveq2d	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to S \underset{˙}{\cdot} D (K (N minMatR1 R) (M) K) = S \underset{˙}{\cdot} E (K (N subMat R) (M) K)$
25	20 24	eqtrd	$⊢ (M \in B \land K \in N \land S \in {Base}_{R}) \to D (K (M (N matRRep R) S) K) = S \underset{˙}{\cdot} E (K (N subMat R) (M) K)$

Metamath Proof Explorer

Theorem smadiadetg

Proof