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

Theorem drngui 17974
Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
drngui.b  |-  B  =  ( Base `  R
)
drngui.z  |-  .0.  =  ( 0g `  R )
drngui.r  |-  R  e.  DivRing
Assertion
Ref Expression
drngui  |-  ( B 
\  {  .0.  }
)  =  (Unit `  R )

Proof of Theorem drngui
StepHypRef Expression
1 drngui.r . . . 4  |-  R  e.  DivRing
2 drngui.b . . . . 5  |-  B  =  ( Base `  R
)
3 eqid 2450 . . . . 5  |-  (Unit `  R )  =  (Unit `  R )
4 drngui.z . . . . 5  |-  .0.  =  ( 0g `  R )
52, 3, 4isdrng 17972 . . . 4  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  (Unit `  R )  =  ( B  \  {  .0.  } ) ) )
61, 5mpbi 212 . . 3  |-  ( R  e.  Ring  /\  (Unit `  R )  =  ( B  \  {  .0.  } ) )
76simpri 464 . 2  |-  (Unit `  R )  =  ( B  \  {  .0.  } )
87eqcomi 2459 1  |-  ( B 
\  {  .0.  }
)  =  (Unit `  R )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1443    e. wcel 1886    \ cdif 3400   {csn 3967   ` cfv 5581   Basecbs 15114   0gc0g 15331   Ringcrg 17773  Unitcui 17860   DivRingcdr 17968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-iota 5545  df-fv 5589  df-drng 17970
This theorem is referenced by:  cnflddiv  18991  cnfldinv  18992  cnsubdrglem  19012  cnmgpabl  19022  cnmsubglem  19023  gzrngunit  19026  zringunit  19055  expghm  19060  psgninv  19143  zrhpsgnmhm  19145  amgmlem  23908  dchrghm  24177  dchrabs  24181  sum2dchr  24195  lgseisenlem4  24273  qrngdiv  24455  proot1ex  36072
  Copyright terms: Public domain W3C validator