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

Theorem drngunit 17537
Description: Elementhood in the set of units when  R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
isdrng.b  |-  B  =  ( Base `  R
)
isdrng.u  |-  U  =  (Unit `  R )
isdrng.z  |-  .0.  =  ( 0g `  R )
Assertion
Ref Expression
drngunit  |-  ( R  e.  DivRing  ->  ( X  e.  U  <->  ( X  e.  B  /\  X  =/= 
.0.  ) ) )

Proof of Theorem drngunit
StepHypRef Expression
1 isdrng.b . . . . 5  |-  B  =  ( Base `  R
)
2 isdrng.u . . . . 5  |-  U  =  (Unit `  R )
3 isdrng.z . . . . 5  |-  .0.  =  ( 0g `  R )
41, 2, 3isdrng 17536 . . . 4  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  U  =  ( B 
\  {  .0.  }
) ) )
54simprbi 462 . . 3  |-  ( R  e.  DivRing  ->  U  =  ( B  \  {  .0.  } ) )
65eleq2d 2466 . 2  |-  ( R  e.  DivRing  ->  ( X  e.  U  <->  X  e.  ( B  \  {  .0.  }
) ) )
7 eldifsn 4086 . 2  |-  ( X  e.  ( B  \  {  .0.  } )  <->  ( X  e.  B  /\  X  =/= 
.0.  ) )
86, 7syl6bb 261 1  |-  ( R  e.  DivRing  ->  ( X  e.  U  <->  ( X  e.  B  /\  X  =/= 
.0.  ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1836    =/= wne 2591    \ cdif 3403   {csn 3961   ` cfv 5513   Basecbs 14657   0gc0g 14870   Ringcrg 17334  Unitcui 17424   DivRingcdr 17532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-br 4385  df-iota 5477  df-fv 5521  df-drng 17534
This theorem is referenced by:  drngunz  17547  drnginvrcl  17549  drnginvrn0  17550  drnginvrl  17551  drnginvrr  17552  issubdrg  17590  abvdiv  17622  qsssubdrg  18613  redvr  18767  drnguc1p  22679  lgseisenlem3  23766  ornglmullt  27986  orngrmullt  27987  isarchiofld  27996  qqhval2lem  28150  qqhf  28155  lincreslvec3  33322  isldepslvec2  33325
  Copyright terms: Public domain W3C validator