mdetlap

Description: Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

	Ref	Expression
Hypotheses	madjusmdet.b	$⊢ B = {Base}_{A}$
	madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
	madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
	madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
	madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	madjusmdet.z	$⊢ Z = ℤRHom (R)$
	madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
	madjusmdet.n	$⊢ φ \to N \in ℕ$
	madjusmdet.r	$⊢ φ \to R \in CRing$
	madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
	madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
	madjusmdet.m	$⊢ φ \to M \in B$
Assertion	mdetlap	$⊢ φ \to D (M) = {\sum_{R}}_{j = 1}^{N} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)))$

Proof

Step	Hyp	Ref	Expression
1		madjusmdet.b	$⊢ B = {Base}_{A}$
2		madjusmdet.a	$⊢ A = (1 \dots N) Mat R$
3		madjusmdet.d	$⊢ D = (1 \dots N) maDet R$
4		madjusmdet.k	$⊢ K = (1 \dots N) maAdju R$
5		madjusmdet.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
6		madjusmdet.z	$⊢ Z = ℤRHom (R)$
7		madjusmdet.e	$⊢ E = (1 \dots N - 1) maDet R$
8		madjusmdet.n	$⊢ φ \to N \in ℕ$
9		madjusmdet.r	$⊢ φ \to R \in CRing$
10		madjusmdet.i	$⊢ φ \to I \in (1 \dots N)$
11		madjusmdet.j	$⊢ φ \to J \in (1 \dots N)$
12		madjusmdet.m	$⊢ φ \to M \in B$
13	2 1 3 4 5	mdetlap1	$⊢ (R \in CRing \land M \in B \land I \in (1 \dots N)) \to D (M) = {\sum_{R}}_{j = 1}^{N} ((I M j) \underset{˙}{\cdot} (j K (M) I))$
14	9 12 10 13	syl3anc	$⊢ φ \to D (M) = {\sum_{R}}_{j = 1}^{N} ((I M j) \underset{˙}{\cdot} (j K (M) I))$
15	8	adantr	$⊢ (φ \land j \in (1 \dots N)) \to N \in ℕ$
16	9	adantr	$⊢ (φ \land j \in (1 \dots N)) \to R \in CRing$
17	10	adantr	$⊢ (φ \land j \in (1 \dots N)) \to I \in (1 \dots N)$
18		simpr	$⊢ (φ \land j \in (1 \dots N)) \to j \in (1 \dots N)$
19	12	adantr	$⊢ (φ \land j \in (1 \dots N)) \to M \in B$
20	1 2 3 4 5 6 7 15 16 17 18 19	madjusmdet	$⊢ (φ \land j \in (1 \dots N)) \to j K (M) I = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)$
21	20	oveq2d	$⊢ (φ \land j \in (1 \dots N)) \to (I M j) \underset{˙}{\cdot} (j K (M) I) = (I M j) \underset{˙}{\cdot} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23	2 22 1 17 18 19	matecld	$⊢ (φ \land j \in (1 \dots N)) \to I M j \in {Base}_{R}$
24		crngring	$⊢ R \in CRing \to R \in Ring$
25	6	zrhrhm	$⊢ R \in Ring \to Z \in (ℤ_{ring} RingHom R)$
26		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
27	26 22	rhmf	$⊢ Z \in (ℤ_{ring} RingHom R) \to Z : ℤ ⟶ {Base}_{R}$
28	9 24 25 27	4syl	$⊢ φ \to Z : ℤ ⟶ {Base}_{R}$
29	28	adantr	$⊢ (φ \land j \in (1 \dots N)) \to Z : ℤ ⟶ {Base}_{R}$
30		1zzd	$⊢ (φ \land j \in (1 \dots N)) \to 1 \in ℤ$
31	30	znegcld	$⊢ (φ \land j \in (1 \dots N)) \to - 1 \in ℤ$
32		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
33	32 17	sselid	$⊢ (φ \land j \in (1 \dots N)) \to I \in ℕ$
34	32 18	sselid	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
35	33 34	nnaddcld	$⊢ (φ \land j \in (1 \dots N)) \to I + j \in ℕ$
36	35	nnnn0d	$⊢ (φ \land j \in (1 \dots N)) \to I + j \in ℕ_{0}$
37		zexpcl	$⊢ (- 1 \in ℤ \land I + j \in ℕ_{0}) \to {(- 1)}^{I + j} \in ℤ$
38	31 36 37	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to {(- 1)}^{I + j} \in ℤ$
39	29 38	ffvelcdmd	$⊢ (φ \land j \in (1 \dots N)) \to Z ({(- 1)}^{I + j}) \in {Base}_{R}$
40	22 5	crngcom	$⊢ (R \in CRing \land I M j \in {Base}_{R} \land Z ({(- 1)}^{I + j}) \in {Base}_{R}) \to (I M j) \underset{˙}{\cdot} Z ({(- 1)}^{I + j}) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} (I M j)$
41	16 23 39 40	syl3anc	$⊢ (φ \land j \in (1 \dots N)) \to (I M j) \underset{˙}{\cdot} Z ({(- 1)}^{I + j}) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} (I M j)$
42	41	oveq1d	$⊢ (φ \land j \in (1 \dots N)) \to ((I M j) \underset{˙}{\cdot} Z ({(- 1)}^{I + j})) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j) = (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} (I M j)) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)$
43	16 24	syl	$⊢ (φ \land j \in (1 \dots N)) \to R \in Ring$
44		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
45		eqid	$⊢ I {subMat}_{1} (M) j = I {subMat}_{1} (M) j$
46	2 1 44 45 15 17 18 19	smatcl	$⊢ (φ \land j \in (1 \dots N)) \to I {subMat}_{1} (M) j \in {Base}_{((1 \dots N - 1) Mat R)}$
47		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
48	7 47 44 22	mdetcl	$⊢ (R \in CRing \land I {subMat}_{1} (M) j \in {Base}_{((1 \dots N - 1) Mat R)}) \to E (I {subMat}_{1} (M) j) \in {Base}_{R}$
49	16 46 48	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to E (I {subMat}_{1} (M) j) \in {Base}_{R}$
50	22 5	ringass	$⊢ (R \in Ring \land (I M j \in {Base}_{R} \land Z ({(- 1)}^{I + j}) \in {Base}_{R} \land E (I {subMat}_{1} (M) j) \in {Base}_{R})) \to ((I M j) \underset{˙}{\cdot} Z ({(- 1)}^{I + j})) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j) = (I M j) \underset{˙}{\cdot} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
51	43 23 39 49 50	syl13anc	$⊢ (φ \land j \in (1 \dots N)) \to ((I M j) \underset{˙}{\cdot} Z ({(- 1)}^{I + j})) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j) = (I M j) \underset{˙}{\cdot} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
52	22 5	ringass	$⊢ (R \in Ring \land (Z ({(- 1)}^{I + j}) \in {Base}_{R} \land I M j \in {Base}_{R} \land E (I {subMat}_{1} (M) j) \in {Base}_{R})) \to (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} (I M j)) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
53	43 39 23 49 52	syl13anc	$⊢ (φ \land j \in (1 \dots N)) \to (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} (I M j)) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
54	42 51 53	3eqtr3d	$⊢ (φ \land j \in (1 \dots N)) \to (I M j) \underset{˙}{\cdot} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
55	21 54	eqtrd	$⊢ (φ \land j \in (1 \dots N)) \to (I M j) \underset{˙}{\cdot} (j K (M) I) = Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j))$
56	55	mpteq2dva	$⊢ φ \to (j \in (1 \dots N) ⟼ (I M j) \underset{˙}{\cdot} (j K (M) I)) = (j \in (1 \dots N) ⟼ Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)))$
57	56	oveq2d	$⊢ φ \to {\sum_{R}}_{j = 1}^{N} ((I M j) \underset{˙}{\cdot} (j K (M) I)) = {\sum_{R}}_{j = 1}^{N} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)))$
58	14 57	eqtrd	$⊢ φ \to D (M) = {\sum_{R}}_{j = 1}^{N} (Z ({(- 1)}^{I + j}) \underset{˙}{\cdot} ((I M j) \underset{˙}{\cdot} E (I {subMat}_{1} (M) j)))$

Metamath Proof Explorer

Theorem mdetlap

Proof