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

Theorem drngrng 15847
Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
Assertion
Ref Expression
drngrng  |-  ( R  e.  DivRing  ->  R  e.  Ring )

Proof of Theorem drngrng
StepHypRef Expression
1 eqid 2438 . . 3  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2438 . . 3  |-  (Unit `  R )  =  (Unit `  R )
3 eqid 2438 . . 3  |-  ( 0g
`  R )  =  ( 0g `  R
)
41, 2, 3isdrng 15844 . 2  |-  ( R  e.  DivRing 
<->  ( R  e.  Ring  /\  (Unit `  R )  =  ( ( Base `  R )  \  {
( 0g `  R
) } ) ) )
54simplbi 448 1  |-  ( R  e.  DivRing  ->  R  e.  Ring )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726    \ cdif 3319   {csn 3816   ` cfv 5457   Basecbs 13474   0gc0g 13728   Ringcrg 15665  Unitcui 15749   DivRingcdr 15840
This theorem is referenced by:  drnggrp  15848  drngid  15854  drngunz  15855  drnginvrcl  15857  drnginvrn0  15858  drnginvrl  15859  drnginvrr  15860  drngmul0or  15861  abvtriv  15934  rlmlvec  16282  drngnidl  16305  drnglpir  16329  drngnzr  16338  drngdomn  16368  qsssubdrg  16763  cphsubrglem  19145  drnguc1p  20098  ig1peu  20099  ig1pcl  20103  ig1pdvds  20104  ig1prsp  20105  ply1lpir  20106  padicabv  21329  ofldsqr  24245  ofldchr  24249  zrhunitpreima  24367  elzrhunit  24368  qqhval2lem  24370  qqh0  24373  qqh1  24374  qqhf  24375  qqhghm  24377  qqhrhm  24378  qqhnm  24379  qqhucn  24381  zrhre  24390  qqhre  24391  sdrgacs  27500  cntzsdrg  27501  dvalveclem  31897  dvhlveclem  31980  hlhilsrnglem  32828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 4216  df-iota 5421  df-fv 5465  df-drng 15842
  Copyright terms: Public domain W3C validator