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

Theorem drngui 18525
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 2609 . . . . 5 (Unit‘𝑅) = (Unit‘𝑅)
4 drngui.z . . . . 5 0 = (0g𝑅)
52, 3, 4isdrng 18523 . . . 4 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 })))
61, 5mpbi 218 . . 3 (𝑅 ∈ Ring ∧ (Unit‘𝑅) = (𝐵 ∖ { 0 }))
76simpri 476 . 2 (Unit‘𝑅) = (𝐵 ∖ { 0 })
87eqcomi 2618 1 (𝐵 ∖ { 0 }) = (Unit‘𝑅)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1976  cdif 3536  {csn 4124  cfv 5790  Basecbs 15644  0gc0g 15872  Ringcrg 18319  Unitcui 18411  DivRingcdr 18519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-drng 18521
This theorem is referenced by:  cnflddiv  19544  cnfldinv  19545  cnsubdrglem  19565  cnmgpabl  19575  cnmsubglem  19577  gzrngunit  19580  zringunit  19606  expghm  19611  psgninv  19695  zrhpsgnmhm  19697  amgmlem  24461  dchrghm  24726  dchrabs  24730  sum2dchr  24744  lgseisenlem4  24848  qrngdiv  25058  proot1ex  36622  amgmwlem  42340  amgmlemALT  42341
  Copyright terms: Public domain W3C validator