Theorem drngring 20649

Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011.)

Assertion

Ref	Expression
drngring	⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Proof of Theorem drngring

Step	Hyp	Ref	Expression
1		eqid 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2731	. . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
3		eqid 2731	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4	1, 2, 3	isdrng 20646	. 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)})))
5	4	simplbi 497	1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ∖ cdif 3899  {csn 4576  ‘cfv 6481  Basecbs 17117  0_gc0g 17340  Ringcrg 20149  Unitcui 20271  DivRingcdr 20642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-drng 20644

This theorem is referenced by:  drngringd  20650  drngid  20659  drngunz  20660  drngnzr  20661  drngdomn  20662  drngmcl  20663  drnginvrcl  20666  drnginvrn0  20667  drnginvrl  20669  drnginvrr  20670  drngmul0orOLD  20674  drhmsubc  20694  drngcat  20695  sdrgid  20705  sdrgacs  20714  cntzsdrg  20715  primefld  20718  rlmlvec  21136  drngnidl  21178  drnglpir  21267  qsssubdrg  21361  ofldchr  21511  frlmlvec  21696  frlmphllem  21715  mpllvec  21955  cvsdivcl  25058  qcvs  25072  cphsubrglem  25102  rrxcph  25317  rrx0  25322  drnguc1p  26104  ig1peu  26105  ig1pcl  26109  ig1pdvds  26110  ig1prsp  26111  ply1lpir  26112  padicabv  27566  reofld  33303  rearchi  33306  xrge0slmod  33308  drng0mxidl  33436  drngmxidl  33437  zringfrac  33514  sradrng  33589  drgext0gsca  33599  drgextlsp  33601  rlmdim  33617  rgmoddimOLD  33618  frlmdim  33619  matdim  33623  drngdimgt0  33626  fedgmullem1  33637  fedgmullem2  33638  fedgmul  33639  fldextid  33667  extdg1id  33674  ccfldsrarelvec  33679  zrhunitpreima  33984  elzrhunit  33985  qqhval2lem  33989  qqh0  33992  qqh1  33993  qqhf  33994  qqhghm  33996  qqhrhm  33997  qqhnm  33998  qqhucn  34000  zrhre  34027  qqhre  34028  lindsdom  37653  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  matunitlindf  37657  dvalveclem  41063  dvhlveclem  41146  hlhilsrnglem  41991  fldhmf1  42122  ricdrng1  42560  0prjspnrel  42659  drhmsubcALTV  48359  drngcatALTV  48360  aacllem  49832