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

Theorem isdrng 15565
Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised 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
isdrng  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  U  =  ( B 
\  {  .0.  }
) ) )

Proof of Theorem isdrng
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 fveq2 5563 . . . 4  |-  ( r  =  R  ->  (Unit `  r )  =  (Unit `  R ) )
2 isdrng.u . . . 4  |-  U  =  (Unit `  R )
31, 2syl6eqr 2366 . . 3  |-  ( r  =  R  ->  (Unit `  r )  =  U )
4 fveq2 5563 . . . . 5  |-  ( r  =  R  ->  ( Base `  r )  =  ( Base `  R
) )
5 isdrng.b . . . . 5  |-  B  =  ( Base `  R
)
64, 5syl6eqr 2366 . . . 4  |-  ( r  =  R  ->  ( Base `  r )  =  B )
7 fveq2 5563 . . . . . 6  |-  ( r  =  R  ->  ( 0g `  r )  =  ( 0g `  R
) )
8 isdrng.z . . . . . 6  |-  .0.  =  ( 0g `  R )
97, 8syl6eqr 2366 . . . . 5  |-  ( r  =  R  ->  ( 0g `  r )  =  .0.  )
109sneqd 3687 . . . 4  |-  ( r  =  R  ->  { ( 0g `  r ) }  =  {  .0.  } )
116, 10difeq12d 3329 . . 3  |-  ( r  =  R  ->  (
( Base `  r )  \  { ( 0g `  r ) } )  =  ( B  \  {  .0.  } ) )
123, 11eqeq12d 2330 . 2  |-  ( r  =  R  ->  (
(Unit `  r )  =  ( ( Base `  r )  \  {
( 0g `  r
) } )  <->  U  =  ( B  \  {  .0.  } ) ) )
13 df-drng 15563 . 2  |-  DivRing  =  {
r  e.  Ring  |  (Unit `  r )  =  ( ( Base `  r
)  \  { ( 0g `  r ) } ) }
1412, 13elrab2 2959 1  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  U  =  ( B 
\  {  .0.  }
) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1633    e. wcel 1701    \ cdif 3183   {csn 3674   ` cfv 5292   Basecbs 13195   0gc0g 13449   Ringcrg 15386  Unitcui 15470   DivRingcdr 15561
This theorem is referenced by:  drngunit  15566  drngui  15567  drngrng  15568  isdrng2  15571  drngprop  15572  drngid  15575  opprdrng  15585  drngpropd  15588  issubdrg  15619  drngdomn  16093  fidomndrng  16097  istdrg2  17912  cphreccllem  18667  zrhunitpreima  23557  cntzsdrg  26658
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-drng 15563
  Copyright terms: Public domain W3C validator