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

Theorem drngring 19431
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 2824 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2824 . . 3 (Unit‘𝑅) = (Unit‘𝑅)
3 eqid 2824 . . 3 (0g𝑅) = (0g𝑅)
41, 2, 3isdrng 19428 . 2 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g𝑅)})))
54simplbi 498 1 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2106  cdif 3936  {csn 4563  cfv 6351  Basecbs 16475  0gc0g 16705  Ringcrg 19219  Unitcui 19311  DivRingcdr 19424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-drng 19426
This theorem is referenced by:  drnggrp  19432  drngid  19438  drngunz  19439  drnginvrcl  19441  drnginvrn0  19442  drnginvrl  19443  drnginvrr  19444  drngmul0or  19445  sdrgid  19497  sdrgacs  19502  cntzsdrg  19503  primefld  19506  abvtriv  19534  rlmlvec  19900  drngnidl  19923  drnglpir  19947  drngnzr  19956  drngdomn  19997  qsssubdrg  20520  frlmlvec  20821  frlmphllem  20840  frlmphl  20841  cvsdivcl  23652  qcvs  23666  cphsubrglem  23696  rrxcph  23910  rrx0  23915  drnguc1p  24679  ig1peu  24680  ig1pcl  24684  ig1pdvds  24685  ig1prsp  24686  ply1lpir  24687  padicabv  26120  ofldchr  30802  reofld  30828  rearchi  30830  xrge0slmod  30832  sradrng  30875  drgext0gsca  30881  drgextlsp  30883  rgmoddim  30895  frlmdim  30896  matdim  30900  drngdimgt0  30903  fedgmullem1  30912  fedgmullem2  30913  fedgmul  30914  fldextid  30936  extdg1id  30940  ccfldsrarelvec  30943  zrhunitpreima  31106  elzrhunit  31107  qqhval2lem  31109  qqh0  31112  qqh1  31113  qqhf  31114  qqhghm  31116  qqhrhm  31117  qqhnm  31118  qqhucn  31120  zrhre  31147  qqhre  31148  lindsdom  34754  lindsenlbs  34755  matunitlindflem1  34756  matunitlindflem2  34757  matunitlindf  34758  dvalveclem  38029  dvhlveclem  38112  hlhilsrnglem  38957  0prjspnrel  39131  drhmsubc  44180  drngcat  44181  drhmsubcALTV  44198  drngcatALTV  44199  aacllem  44731
  Copyright terms: Public domain W3C validator