Theorem drngring 20669

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3898  {csn 4580  ‘cfv 6492  Basecbs 17136  0_gc0g 17359  Ringcrg 20168  Unitcui 20291  DivRingcdr 20662

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-drng 20664

This theorem is referenced by:  drngringd  20670  drngid  20679  drngunz  20680  drngnzr  20681  drngdomn  20682  drngmcl  20683  drnginvrcl  20686  drnginvrn0  20687  drnginvrl  20689  drnginvrr  20690  drngmul0orOLD  20694  drhmsubc  20714  drngcat  20715  sdrgid  20725  sdrgacs  20734  cntzsdrg  20735  primefld  20738  rlmlvec  21156  drngnidl  21198  drnglpir  21287  qsssubdrg  21381  ofldchr  21531  frlmlvec  21716  frlmphllem  21735  mpllvec  21975  cvsdivcl  25089  qcvs  25103  cphsubrglem  25133  rrxcph  25348  rrx0  25353  drnguc1p  26135  ig1peu  26136  ig1pcl  26140  ig1pdvds  26141  ig1prsp  26142  ply1lpir  26143  padicabv  27597  reofld  33424  rearchi  33427  xrge0slmod  33429  drng0mxidl  33557  drngmxidl  33558  zringfrac  33635  sradrng  33738  drgext0gsca  33748  drgextlsp  33750  rlmdim  33766  rgmoddimOLD  33767  frlmdim  33768  matdim  33772  drngdimgt0  33775  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  fldextid  33816  extdg1id  33823  ccfldsrarelvec  33828  zrhunitpreima  34133  elzrhunit  34134  qqhval2lem  34138  qqh0  34141  qqh1  34142  qqhf  34143  qqhghm  34145  qqhrhm  34146  qqhnm  34147  qqhucn  34149  zrhre  34176  qqhre  34177  lindsdom  37811  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  matunitlindf  37815  dvalveclem  41281  dvhlveclem  41364  hlhilsrnglem  42209  fldhmf1  42340  ricdrng1  42779  0prjspnrel  42866  drhmsubcALTV  48571  drngcatALTV  48572  aacllem  50042