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

Theorem isdrng 17176
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 5857 . . . 4  |-  ( r  =  R  ->  (Unit `  r )  =  (Unit `  R ) )
2 isdrng.u . . . 4  |-  U  =  (Unit `  R )
31, 2syl6eqr 2519 . . 3  |-  ( r  =  R  ->  (Unit `  r )  =  U )
4 fveq2 5857 . . . . 5  |-  ( r  =  R  ->  ( Base `  r )  =  ( Base `  R
) )
5 isdrng.b . . . . 5  |-  B  =  ( Base `  R
)
64, 5syl6eqr 2519 . . . 4  |-  ( r  =  R  ->  ( Base `  r )  =  B )
7 fveq2 5857 . . . . . 6  |-  ( r  =  R  ->  ( 0g `  r )  =  ( 0g `  R
) )
8 isdrng.z . . . . . 6  |-  .0.  =  ( 0g `  R )
97, 8syl6eqr 2519 . . . . 5  |-  ( r  =  R  ->  ( 0g `  r )  =  .0.  )
109sneqd 4032 . . . 4  |-  ( r  =  R  ->  { ( 0g `  r ) }  =  {  .0.  } )
116, 10difeq12d 3616 . . 3  |-  ( r  =  R  ->  (
( Base `  r )  \  { ( 0g `  r ) } )  =  ( B  \  {  .0.  } ) )
123, 11eqeq12d 2482 . 2  |-  ( r  =  R  ->  (
(Unit `  r )  =  ( ( Base `  r )  \  {
( 0g `  r
) } )  <->  U  =  ( B  \  {  .0.  } ) ) )
13 df-drng 17174 . 2  |-  DivRing  =  {
r  e.  Ring  |  (Unit `  r )  =  ( ( Base `  r
)  \  { ( 0g `  r ) } ) }
1412, 13elrab2 3256 1  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  U  =  ( B 
\  {  .0.  }
) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762    \ cdif 3466   {csn 4020   ` cfv 5579   Basecbs 14479   0gc0g 14684   Ringcrg 16979  Unitcui 17065   DivRingcdr 17172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-drng 17174
This theorem is referenced by:  drngunit  17177  drngui  17178  drngrng  17179  isdrng2  17182  drngprop  17183  drngid  17186  opprdrng  17196  drngpropd  17199  issubdrg  17230  drngdomn  17716  fidomndrng  17720  istdrg2  20408  cvsunit  21336  cphreccllem  21353  zrhunitpreima  27581  cntzsdrg  30745
  Copyright terms: Public domain W3C validator