Theorem drngring 20639

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 2729	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2729	. . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
3		eqid 2729	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4	1, 2, 3	isdrng 20636	. 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)})))
5	4	simplbi 497	1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∖ cdif 3902  {csn 4579  ‘cfv 6486  Basecbs 17138  0_gc0g 17361  Ringcrg 20136  Unitcui 20258  DivRingcdr 20632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-drng 20634

This theorem is referenced by:  drngringd  20640  drngid  20649  drngunz  20650  drngnzr  20651  drngdomn  20652  drngmcl  20653  drnginvrcl  20656  drnginvrn0  20657  drnginvrl  20659  drnginvrr  20660  drngmul0orOLD  20664  drhmsubc  20684  drngcat  20685  sdrgid  20695  sdrgacs  20704  cntzsdrg  20705  primefld  20708  rlmlvec  21126  drngnidl  21168  drnglpir  21257  qsssubdrg  21351  ofldchr  21501  frlmlvec  21686  frlmphllem  21705  mpllvec  21945  cvsdivcl  25049  qcvs  25063  cphsubrglem  25093  rrxcph  25308  rrx0  25313  drnguc1p  26095  ig1peu  26096  ig1pcl  26100  ig1pdvds  26101  ig1prsp  26102  ply1lpir  26103  padicabv  27557  reofld  33291  rearchi  33293  xrge0slmod  33295  drng0mxidl  33423  drngmxidl  33424  zringfrac  33501  sradrng  33554  drgext0gsca  33563  drgextlsp  33565  rlmdim  33581  rgmoddimOLD  33582  frlmdim  33583  matdim  33587  drngdimgt0  33590  fedgmullem1  33601  fedgmullem2  33602  fedgmul  33603  fldextid  33631  extdg1id  33637  ccfldsrarelvec  33642  zrhunitpreima  33942  elzrhunit  33943  qqhval2lem  33947  qqh0  33950  qqh1  33951  qqhf  33952  qqhghm  33954  qqhrhm  33955  qqhnm  33956  qqhucn  33958  zrhre  33985  qqhre  33986  lindsdom  37593  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  dvalveclem  41004  dvhlveclem  41087  hlhilsrnglem  41932  fldhmf1  42063  ricdrng1  42501  0prjspnrel  42600  drhmsubcALTV  48314  drngcatALTV  48315  aacllem  49787