Metamath Proof Explorer

Theorem mdetr0

Description: The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mdetr0.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
mdetr0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mdetr0.z ⊢ 0 = ( 0g ‘ 𝑅 )
mdetr0.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mdetr0.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mdetr0.x ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
mdetr0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
Assertion mdetr0 ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) = 0 )

Proof

Step Hyp Ref Expression
1 mdetr0.d ⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2 mdetr0.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 mdetr0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mdetr0.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 mdetr0.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
6 mdetr0.x ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑋 ∈ 𝐾 )
7 mdetr0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 4 9 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
11 2 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
12 10 11 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
13 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 0 ∈ 𝐾 )
14 1 2 8 4 5 13 6 12 7 mdetrsca2 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 0 ( .r ‘ 𝑅 ) 0 ) , 𝑋 ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) ) )
15 2 8 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ 𝐾 ) → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
16 10 12 15 syl2anc ⊢ ( 𝜑 → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
17 16 ifeq1d ⊢ ( 𝜑 → if ( 𝑖 = 𝐼 , ( 0 ( .r ‘ 𝑅 ) 0 ) , 𝑋 ) = if ( 𝑖 = 𝐼 , 0 , 𝑋 ) )
18 17 mpoeq3dv ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 0 ( .r ‘ 𝑅 ) 0 ) , 𝑋 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) )
19 18 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , ( 0 ( .r ‘ 𝑅 ) 0 ) , 𝑋 ) ) ) = ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) )
20 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
21 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
22 1 20 21 2 mdetf ⊢ ( 𝑅 ∈ CRing → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
23 4 22 syl ⊢ ( 𝜑 → 𝐷 : ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ⟶ 𝐾 )
24 13 6 ifcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ∈ 𝐾 )
25 20 2 21 5 4 24 matbas2d ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
26 23 25 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) ∈ 𝐾 )
27 2 8 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) ∈ 𝐾 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) ) = 0 )
28 10 26 27 syl2anc ⊢ ( 𝜑 → ( 0 ( .r ‘ 𝑅 ) ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) ) = 0 )
29 14 19 28 3eqtr3d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐼 , 0 , 𝑋 ) ) ) = 0 )