mdet0

Description: The determinant of the zero matrix (of dimension greater 0!) is 0. (Contributed by AV, 17-Aug-2019) (Revised by AV, 3-Jul-2022)

	Ref	Expression
Hypotheses	mdet0.d	$⊢ D = N maDet R$
	mdet0.a	$⊢ A = N Mat R$
	mdet0.z	$⊢ Z = 0_{A}$
	mdet0.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	mdet0	$⊢ (R \in CRing \land N \in Fin \land N \neq \emptyset) \to D (Z) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		mdet0.d	$⊢ D = N maDet R$
2		mdet0.a	$⊢ A = N Mat R$
3		mdet0.z	$⊢ Z = 0_{A}$
4		mdet0.0	$⊢ \underset{˙}{0} = 0_{R}$
5		n0	$⊢ N \neq \emptyset \leftrightarrow \exists i i \in N$
6		crngring	$⊢ R \in CRing \to R \in Ring$
7	6	anim1ci	$⊢ (R \in CRing \land N \in Fin) \to (N \in Fin \land R \in Ring)$
8	7	adantr	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to (N \in Fin \land R \in Ring)$
9	2 4	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (x \in N, y \in N ⟼ \underset{˙}{0})$
10	3 9	syl5eq	$⊢ (N \in Fin \land R \in Ring) \to Z = (x \in N, y \in N ⟼ \underset{˙}{0})$
11	8 10	syl	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to Z = (x \in N, y \in N ⟼ \underset{˙}{0})$
12	11	fveq2d	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to D (Z) = D ((x \in N, y \in N ⟼ \underset{˙}{0}))$
13		ifid	$⊢ if (x = i, \underset{˙}{0}, \underset{˙}{0}) = \underset{˙}{0}$
14	13	eqcomi	$⊢ \underset{˙}{0} = if (x = i, \underset{˙}{0}, \underset{˙}{0})$
15	14	a1i	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to \underset{˙}{0} = if (x = i, \underset{˙}{0}, \underset{˙}{0})$
16	15	mpoeq3dv	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to (x \in N, y \in N ⟼ \underset{˙}{0}) = (x \in N, y \in N ⟼ if (x = i, \underset{˙}{0}, \underset{˙}{0}))$
17	16	fveq2d	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to D ((x \in N, y \in N ⟼ \underset{˙}{0})) = D ((x \in N, y \in N ⟼ if (x = i, \underset{˙}{0}, \underset{˙}{0})))$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19		simpll	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to R \in CRing$
20		simpr	$⊢ (R \in CRing \land N \in Fin) \to N \in Fin$
21	20	adantr	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to N \in Fin$
22		ringmnd	$⊢ R \in Ring \to R \in Mnd$
23	6 22	syl	$⊢ R \in CRing \to R \in Mnd$
24	23	adantr	$⊢ (R \in CRing \land N \in Fin) \to R \in Mnd$
25	18 4	mndidcl	$⊢ R \in Mnd \to \underset{˙}{0} \in {Base}_{R}$
26	24 25	syl	$⊢ (R \in CRing \land N \in Fin) \to \underset{˙}{0} \in {Base}_{R}$
27	26	adantr	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to \underset{˙}{0} \in {Base}_{R}$
28	27	3ad2ant1	$⊢ (((R \in CRing \land N \in Fin) \land i \in N) \land x \in N \land y \in N) \to \underset{˙}{0} \in {Base}_{R}$
29		simpr	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to i \in N$
30	1 18 4 19 21 28 29	mdetr0	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to D ((x \in N, y \in N ⟼ if (x = i, \underset{˙}{0}, \underset{˙}{0}))) = \underset{˙}{0}$
31	12 17 30	3eqtrd	$⊢ ((R \in CRing \land N \in Fin) \land i \in N) \to D (Z) = \underset{˙}{0}$
32	31	ex	$⊢ (R \in CRing \land N \in Fin) \to (i \in N \to D (Z) = \underset{˙}{0})$
33	32	exlimdv	$⊢ (R \in CRing \land N \in Fin) \to (\exists i i \in N \to D (Z) = \underset{˙}{0})$
34	5 33	syl5bi	$⊢ (R \in CRing \land N \in Fin) \to (N \neq \emptyset \to D (Z) = \underset{˙}{0})$
35	34	3impia	$⊢ (R \in CRing \land N \in Fin \land N \neq \emptyset) \to D (Z) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem mdet0

Proof