Theorem drngring 20871

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ∖ cdif 3905  {csn 4594  ‘cfv 6543  Basecbs 17294  0_gc0g 17517  Ringcrg 20346  Unitcui 20470  DivRingcdr 20864

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-drng 20866

This theorem is used by:  drngringd  20872  drngid  20883  drngunz  20884  drngnzr  20885  drngdomn  20886  drngmcl  20892  drnginvrcl  20894  drnginvrn0  20895  drnginvrl  20897  drnginvrr  20898  drhmsubc  20921  drngcat  20922  sdrgid  20932  sdrgacs  20941  cntzsdrg  20942  primefld  20945  rlmlvec  21362  drngnidl  21414  drnglpir  21537  qsssubdrg  21613  ofldchr  21763  frlmlvec  21948  frlmphllem  21967  mpllvec  22206  cvsdivcl  25329  qcvs  25343  cphsubrglem  25373  rrxcph  25588  rrx0  25593  drnguc1p  26368  ig1peu  26369  ig1pcl  26373  ig1pdvds  26374  ig1prsp  26375  ply1lpir  26376  padicabv  27831  reofld  33694  rearchi  33697  xrge0slmod  33699  drng0mxidl  33789  drngmxidl  33790  zringfrac  33875  sradrng  34003  drgext0gsca  34013  drgextlsp  34015  rlmdim  34031  frlmdim  34032  matdim  34036  drngdimgt0  34039  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  fldextid  34080  extdg1id  34087  ccfldsrarelvec  34092  zrhunitpreima  34397  elzrhunit  34398  qqhval2lem  34402  qqh0  34405  qqh1  34406  qqhf  34407  qqhghm  34409  qqhrhm  34410  qqhnm  34411  qqhucn  34413  zrhre  34440  qqhre  34441  lindsdom  38305  lindsenlbs  38306  matunitlindflem1  38307  matunitlindflem2  38308  matunitlindf  38309  dvalveclem  41839  dvhlveclem  41922  hlhilsrnglem  42767  fldhmf1  42897  ricdrng1  43336  0prjspnrel  43399  drhmsubcALTV  49134  drngcatALTV  49135  aacllem  50661