Metamath Proof Explorer

Theorem dmatelnd

Description: An extradiagonal entry of a diagonal matrix is equal to zero. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatelnd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) ) → ( 𝐼 𝑋 𝐽 ) = 0 )

Proof

Step Hyp Ref Expression
1 dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5 1 2 3 4 dmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) ) ) )
6 neeq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ≠ 𝑗 ↔ 𝐼 ≠ 𝑗 ) )
7 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 𝑋 𝑗 ) = ( 𝐼 𝑋 𝑗 ) )
8 7 eqeq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 𝑋 𝑗 ) = 0 ↔ ( 𝐼 𝑋 𝑗 ) = 0 ) )
9 6 8 imbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) ↔ ( 𝐼 ≠ 𝑗 → ( 𝐼 𝑋 𝑗 ) = 0 ) ) )
10 neeq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐼 ≠ 𝑗 ↔ 𝐼 ≠ 𝐽 ) )
11 oveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐼 𝑋 𝑗 ) = ( 𝐼 𝑋 𝐽 ) )
12 11 eqeq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 𝑋 𝑗 ) = 0 ↔ ( 𝐼 𝑋 𝐽 ) = 0 ) )
13 10 12 imbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ≠ 𝑗 → ( 𝐼 𝑋 𝑗 ) = 0 ) ↔ ( 𝐼 ≠ 𝐽 → ( 𝐼 𝑋 𝐽 ) = 0 ) ) )
14 9 13 rspc2v ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) → ( 𝐼 ≠ 𝐽 → ( 𝐼 𝑋 𝐽 ) = 0 ) ) )
15 14 com23 ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( 𝐼 ≠ 𝐽 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) ) )
16 15 3impia ⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) )
17 16 com12 ⊢ ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) )
18 17 2a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐵 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) ) ) )
19 18 impd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑋 𝑗 ) = 0 ) ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) ) )
20 5 19 sylbid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) ) )
21 20 3impia ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐼 𝑋 𝐽 ) = 0 ) )
22 21 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽 ) ) → ( 𝐼 𝑋 𝐽 ) = 0 )