Theorem 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	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
	mdet0.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mdet0.z	⊢ 𝑍 = ( 0g ‘ 𝐴 )
	mdet0.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	mdet0	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) → ( 𝐷 ‘ 𝑍 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mdet0.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		mdet0.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mdet0.z	⊢ 𝑍 = ( 0g ‘ 𝐴 )
4		mdet0.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		n0	⊢ ( 𝑁 ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ 𝑁 )
6		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7	6	anim1ci	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
8	7	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
9	2 4	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) )
10	3 9	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑍 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) )
11	8 10	syl	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 𝑍 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) )
12	11	fveq2d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑍 ) = ( 𝐷 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) ) )
13		ifid	⊢ if ( 𝑥 = 𝑖 , 0 , 0 ) = 0
14	13	eqcomi	⊢ 0 = if ( 𝑥 = 𝑖 , 0 , 0 )
15	14	a1i	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 0 = if ( 𝑥 = 𝑖 , 0 , 0 ) )
16	15	mpoeq3dv	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑖 , 0 , 0 ) ) )
17	16	fveq2d	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ 0 ) ) = ( 𝐷 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑖 , 0 , 0 ) ) ) )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19		simpll	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ CRing )
20		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑁 ∈ Fin )
21	20	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
22		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
23	6 22	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Mnd )
24	23	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ Mnd )
25	18 4	mndidcl	⊢ ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
26	24 25	syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 0 ∈ ( Base ‘ 𝑅 ) )
27	26	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 0 ∈ ( Base ‘ 𝑅 ) )
28	27	3ad2ant1	⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 0 ∈ ( Base ‘ 𝑅 ) )
29		simpr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
30	1 18 4 19 21 28 29	mdetr0	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐷 ‘ ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑖 , 0 , 0 ) ) ) = 0 )
31	12 17 30	3eqtrd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) ∧ 𝑖 ∈ 𝑁 ) → ( 𝐷 ‘ 𝑍 ) = 0 )
32	31	ex	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑁 → ( 𝐷 ‘ 𝑍 ) = 0 ) )
33	32	exlimdv	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ∃ 𝑖 𝑖 ∈ 𝑁 → ( 𝐷 ‘ 𝑍 ) = 0 ) )
34	5 33	syl5bi	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑁 ≠ ∅ → ( 𝐷 ‘ 𝑍 ) = 0 ) )
35	34	3impia	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) → ( 𝐷 ‘ 𝑍 ) = 0 )