MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  drngring Structured version   Visualization version   GIF version

Theorem drngring 19438
Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
Assertion
Ref Expression
drngring (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Proof of Theorem drngring
StepHypRef Expression
1 eqid 2818 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2818 . . 3 (Unit‘𝑅) = (Unit‘𝑅)
3 eqid 2818 . . 3 (0g𝑅) = (0g𝑅)
41, 2, 3isdrng 19435 . 2 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g𝑅)})))
54simplbi 498 1 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  cdif 3930  {csn 4557  cfv 6348  Basecbs 16471  0gc0g 16701  Ringcrg 19226  Unitcui 19318  DivRingcdr 19431
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-drng 19433
This theorem is referenced by:  drnggrp  19439  drngid  19445  drngunz  19446  drnginvrcl  19448  drnginvrn0  19449  drnginvrl  19450  drnginvrr  19451  drngmul0or  19452  sdrgid  19504  sdrgacs  19509  cntzsdrg  19510  primefld  19513  abvtriv  19541  rlmlvec  19907  drngnidl  19930  drnglpir  19954  drngnzr  19963  drngdomn  20004  mpllvec  20161  qsssubdrg  20532  frlmlvec  20833  frlmphllem  20852  frlmphl  20853  cvsdivcl  23664  qcvs  23678  cphsubrglem  23708  rrxcph  23922  rrx0  23927  drnguc1p  24691  ig1peu  24692  ig1pcl  24696  ig1pdvds  24697  ig1prsp  24698  ply1lpir  24699  padicabv  26133  ofldchr  30814  reofld  30840  rearchi  30842  xrge0slmod  30844  sradrng  30887  drgext0gsca  30893  drgextlsp  30895  rgmoddim  30907  frlmdim  30908  matdim  30912  drngdimgt0  30915  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  fldextid  30948  extdg1id  30952  ccfldsrarelvec  30955  zrhunitpreima  31118  elzrhunit  31119  qqhval2lem  31121  qqh0  31124  qqh1  31125  qqhf  31126  qqhghm  31128  qqhrhm  31129  qqhnm  31130  qqhucn  31132  zrhre  31159  qqhre  31160  lindsdom  34767  lindsenlbs  34768  matunitlindflem1  34769  matunitlindflem2  34770  matunitlindf  34771  dvalveclem  38041  dvhlveclem  38124  hlhilsrnglem  38969  0prjspnrel  39147  drhmsubc  44279  drngcat  44280  drhmsubcALTV  44297  drngcatALTV  44298  aacllem  44830
  Copyright terms: Public domain W3C validator