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	9 24	syl	$⊢ φ \to R \in Ring$
26	6	zrhrhm	$⊢ R \in Ring \to Z \in (ℤ_{ring} RingHom R)$
27		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
28	27 22	rhmf	$⊢ Z \in (ℤ_{ring} RingHom R) \to Z : ℤ ⟶ {Base}_{R}$
29	25 26 28	3syl	$⊢ φ \to Z : ℤ ⟶ {Base}_{R}$
30	29	adantr	$⊢ (φ \land j \in (1 \dots N)) \to Z : ℤ ⟶ {Base}_{R}$
31		1zzd	$⊢ (φ \land j \in (1 \dots N)) \to 1 \in ℤ$
32	31	znegcld	$⊢ (φ \land j \in (1 \dots N)) \to - 1 \in ℤ$
33		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
34	33 17	sseldi	$⊢ (φ \land j \in (1 \dots N)) \to I \in ℕ$
35	33 18	sseldi	$⊢ (φ \land j \in (1 \dots N)) \to j \in ℕ$
36	34 35	nnaddcld	$⊢ (φ \land j \in (1 \dots N)) \to I + j \in ℕ$
37	36	nnnn0d	$⊢ (φ \land j \in (1 \dots N)) \to I + j \in ℕ_{0}$
38		zexpcl	$⊢ (- 1 \in ℤ \land I + j \in ℕ_{0}) \to {(- 1)}^{I + j} \in ℤ$
39	32 37 38	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to {(- 1)}^{I + j} \in ℤ$
40	30 39	ffvelrnd	$⊢ (φ \land j \in (1 \dots N)) \to Z ({(- 1)}^{I + j}) \in {Base}_{R}$
41	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)$
42	16 23 40 41	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)$
43	42	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)$
44	16 24	syl	$⊢ (φ \land j \in (1 \dots N)) \to R \in Ring$
45		eqid	$⊢ {Base}_{((1 \dots N - 1) Mat R)} = {Base}_{((1 \dots N - 1) Mat R)}$
46		eqid	$⊢ I {subMat}_{1} (M) j = I {subMat}_{1} (M) j$
47	2 1 45 46 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)}$
48		eqid	$⊢ (1 \dots N - 1) Mat R = (1 \dots N - 1) Mat R$
49	7 48 45 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}$
50	16 47 49	syl2anc	$⊢ (φ \land j \in (1 \dots N)) \to E (I {subMat}_{1} (M) j) \in {Base}_{R}$
51	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))$
52	44 23 40 50 51	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))$
53	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))$
54	44 40 23 50 53	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))$
55	43 52 54	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))$
56	21 55	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))$
57	56	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)))$
58	57	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)))$
59	14 58	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