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

Theorem drngunit 18975
Description: Elementhood in the set of units when 𝑅 is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
isdrng.b 𝐵 = (Base‘𝑅)
isdrng.u 𝑈 = (Unit‘𝑅)
isdrng.z 0 = (0g𝑅)
Assertion
Ref Expression
drngunit (𝑅 ∈ DivRing → (𝑋𝑈 ↔ (𝑋𝐵𝑋0 )))

Proof of Theorem drngunit
StepHypRef Expression
1 isdrng.b . . . . 5 𝐵 = (Base‘𝑅)
2 isdrng.u . . . . 5 𝑈 = (Unit‘𝑅)
3 isdrng.z . . . . 5 0 = (0g𝑅)
41, 2, 3isdrng 18974 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
54simprbi 486 . . 3 (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
65eleq2d 2882 . 2 (𝑅 ∈ DivRing → (𝑋𝑈𝑋 ∈ (𝐵 ∖ { 0 })))
7 eldifsn 4519 . 2 (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋𝐵𝑋0 ))
86, 7syl6bb 278 1 (𝑅 ∈ DivRing → (𝑋𝑈 ↔ (𝑋𝐵𝑋0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wne 2989  cdif 3777  {csn 4381  cfv 6110  Basecbs 16087  0gc0g 16324  Ringcrg 18768  Unitcui 18860  DivRingcdr 18970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118  df-drng 18972
This theorem is referenced by:  drngunz  18985  drnginvrcl  18987  drnginvrn0  18988  drnginvrl  18989  drnginvrr  18990  issubdrg  19028  abvdiv  19060  qsssubdrg  20032  redvr  20191  drnguc1p  24166  lgseisenlem3  25338  ornglmullt  30154  orngrmullt  30155  isarchiofld  30164  qqhval2lem  30372  qqhf  30377  matunitlindf  33738  lincreslvec3  42856  isldepslvec2  42859
  Copyright terms: Public domain W3C validator