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

Theorem drngui 18955
Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
drngui.b 𝐵 = (Base‘𝑅)
drngui.z 0 = (0g𝑅)
drngui.r 𝑅 ∈ DivRing
Assertion
Ref Expression
drngui (𝐵 ∖ { 0 }) = (Unit‘𝑅)

Proof of Theorem drngui
StepHypRef Expression
1 drngui.r . . . 4 𝑅 ∈ DivRing
2 drngui.b . . . . 5 𝐵 = (Base‘𝑅)
3 eqid 2804 . . . . 5 (Unit‘𝑅) = (Unit‘𝑅)
4 drngui.z . . . . 5 0 = (0g𝑅)
52, 3, 4isdrng 18953 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })))
61, 5mpbi 221 . . 3 (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))
76simpri 475 . 2 (Unit‘𝑅) = (𝐵 ∖ { 0 })
87eqcomi 2813 1 (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wcel 2156  cdif 3764  {csn 4368  cfv 6099  Basecbs 16066  0gc0g 16303  Ringcrg 18747  Unitcui 18839  DivRingcdr 18949
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
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 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ral 3099  df-rex 3100  df-rab 3103  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4843  df-iota 6062  df-fv 6107  df-drng 18951
This theorem is referenced by:  cnflddiv  19982  cnfldinv  19983  cnsubdrglem  20003  cnmgpabl  20013  cnmsubglem  20015  gzrngunit  20018  zringunit  20042  expghm  20050  psgninv  20133  zrhpsgnmhm  20135  amgmlem  24928  dchrghm  25193  dchrabs  25197  sum2dchr  25211  lgseisenlem4  25315  qrngdiv  25525  proot1ex  38278  amgmwlem  43117  amgmlemALT  43118
  Copyright terms: Public domain W3C validator