This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝑁 ∈ 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 biimtrid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( 𝑁 ≠ ∅ → ( 𝐷 ‘ 𝑍 ) = 0 ) )
35 34 3impia ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ) → ( 𝐷 ‘ 𝑍 ) = 0 )