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