MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmatelnd Structured version   Visualization version   GIF version

Theorem dmatelnd 20540
Description: An extradiagonal entry of a diagonal matrix is equal to zero. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
Hypotheses
Ref Expression
dmatid.a 𝐴 = (𝑁 Mat 𝑅)
dmatid.b 𝐵 = (Base‘𝐴)
dmatid.0 0 = (0g𝑅)
dmatid.d 𝐷 = (𝑁 DMat 𝑅)
Assertion
Ref Expression
dmatelnd (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷) ∧ (𝐼𝑁𝐽𝑁𝐼𝐽)) → (𝐼𝑋𝐽) = 0 )

Proof of Theorem dmatelnd
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmatid.a . . . . 5 𝐴 = (𝑁 Mat 𝑅)
2 dmatid.b . . . . 5 𝐵 = (Base‘𝐴)
3 dmatid.0 . . . . 5 0 = (0g𝑅)
4 dmatid.d . . . . 5 𝐷 = (𝑁 DMat 𝑅)
51, 2, 3, 4dmatel 20537 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋𝐷 ↔ (𝑋𝐵 ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ))))
6 neeq1 3008 . . . . . . . . . . 11 (𝑖 = 𝐼 → (𝑖𝑗𝐼𝑗))
7 oveq1 6819 . . . . . . . . . . . 12 (𝑖 = 𝐼 → (𝑖𝑋𝑗) = (𝐼𝑋𝑗))
87eqeq1d 2776 . . . . . . . . . . 11 (𝑖 = 𝐼 → ((𝑖𝑋𝑗) = 0 ↔ (𝐼𝑋𝑗) = 0 ))
96, 8imbi12d 334 . . . . . . . . . 10 (𝑖 = 𝐼 → ((𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) ↔ (𝐼𝑗 → (𝐼𝑋𝑗) = 0 )))
10 neeq2 3009 . . . . . . . . . . 11 (𝑗 = 𝐽 → (𝐼𝑗𝐼𝐽))
11 oveq2 6820 . . . . . . . . . . . 12 (𝑗 = 𝐽 → (𝐼𝑋𝑗) = (𝐼𝑋𝐽))
1211eqeq1d 2776 . . . . . . . . . . 11 (𝑗 = 𝐽 → ((𝐼𝑋𝑗) = 0 ↔ (𝐼𝑋𝐽) = 0 ))
1310, 12imbi12d 334 . . . . . . . . . 10 (𝑗 = 𝐽 → ((𝐼𝑗 → (𝐼𝑋𝑗) = 0 ) ↔ (𝐼𝐽 → (𝐼𝑋𝐽) = 0 )))
149, 13rspc2v 3478 . . . . . . . . 9 ((𝐼𝑁𝐽𝑁) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) → (𝐼𝐽 → (𝐼𝑋𝐽) = 0 )))
1514com23 86 . . . . . . . 8 ((𝐼𝑁𝐽𝑁) → (𝐼𝐽 → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) → (𝐼𝑋𝐽) = 0 )))
16153impia 1136 . . . . . . 7 ((𝐼𝑁𝐽𝑁𝐼𝐽) → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) → (𝐼𝑋𝐽) = 0 ))
1716com12 32 . . . . . 6 (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) → ((𝐼𝑁𝐽𝑁𝐼𝐽) → (𝐼𝑋𝐽) = 0 ))
18172a1i 12 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋𝐵 → (∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 ) → ((𝐼𝑁𝐽𝑁𝐼𝐽) → (𝐼𝑋𝐽) = 0 ))))
1918impd 397 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑋𝐵 ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝑋𝑗) = 0 )) → ((𝐼𝑁𝐽𝑁𝐼𝐽) → (𝐼𝑋𝐽) = 0 )))
205, 19sylbid 231 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋𝐷 → ((𝐼𝑁𝐽𝑁𝐼𝐽) → (𝐼𝑋𝐽) = 0 )))
21203impia 1136 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷) → ((𝐼𝑁𝐽𝑁𝐼𝐽) → (𝐼𝑋𝐽) = 0 ))
2221imp 394 1 (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷) ∧ (𝐼𝑁𝐽𝑁𝐼𝐽)) → (𝐼𝑋𝐽) = 0 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1098   = wceq 1634  wcel 2148  wne 2946  wral 3064  cfv 6042  (class class class)co 6812  Fincfn 8130  Basecbs 16084  0gc0g 16328  Ringcrg 18775   Mat cmat 20450   DMat cdmat 20532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-iota 6005  df-fun 6044  df-fv 6050  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-dmat 20534
This theorem is referenced by:  dmatmul  20541  dmatsubcl  20542
  Copyright terms: Public domain W3C validator