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

Theorem drngui 15843
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 2438 . . . . 5  |-  (Unit `  R )  =  (Unit `  R )
4 drngui.z . . . . 5  |-  .0.  =  ( 0g `  R )
52, 3, 4isdrng 15841 . . . 4  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  (Unit `  R )  =  ( B  \  {  .0.  } ) ) )
61, 5mpbi 201 . . 3  |-  ( R  e.  Ring  /\  (Unit `  R )  =  ( B  \  {  .0.  } ) )
76simpri 450 . 2  |-  (Unit `  R )  =  ( B  \  {  .0.  } )
87eqcomi 2442 1  |-  ( B 
\  {  .0.  }
)  =  (Unit `  R )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1653    e. wcel 1726    \ cdif 3319   {csn 3816   ` cfv 5456   Basecbs 13471   0gc0g 13725   Ringcrg 15662  Unitcui 15746   DivRingcdr 15837
This theorem is referenced by:  cnflddiv  16733  cnfldinv  16734  cnsubdrglem  16751  cnmgpabl  16762  cnmsubglem  16763  gzrngunit  16766  zrngunit  16767  expghm  16779  amgmlem  20830  dchrghm  21042  dchrabs  21046  sum2dchr  21060  lgseisenlem4  21138  qrngdiv  21320  proot1ex  27499
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-drng 15839
  Copyright terms: Public domain W3C validator