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

Theorem drngunit 18962
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 18961 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝑈 = (𝐵 ∖ { 0 })))
54simprbi 484 . . 3 (𝑅 ∈ DivRing → 𝑈 = (𝐵 ∖ { 0 }))
65eleq2d 2836 . 2 (𝑅 ∈ DivRing → (𝑋𝑈𝑋 ∈ (𝐵 ∖ { 0 })))
7 eldifsn 4453 . 2 (𝑋 ∈ (𝐵 ∖ { 0 }) ↔ (𝑋𝐵𝑋0 ))
86, 7syl6bb 276 1 (𝑅 ∈ DivRing → (𝑋𝑈 ↔ (𝑋𝐵𝑋0 )))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  wne 2943  cdif 3720  {csn 4316  cfv 6031  Basecbs 16064  0gc0g 16308  Ringcrg 18755  Unitcui 18847  DivRingcdr 18957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-drng 18959
This theorem is referenced by:  drngunz  18972  drnginvrcl  18974  drnginvrn0  18975  drnginvrl  18976  drnginvrr  18977  issubdrg  19015  abvdiv  19047  qsssubdrg  20020  redvr  20180  drnguc1p  24150  lgseisenlem3  25323  ornglmullt  30147  orngrmullt  30148  isarchiofld  30157  qqhval2lem  30365  qqhf  30370  matunitlindf  33740  lincreslvec3  42799  isldepslvec2  42802
  Copyright terms: Public domain W3C validator