Theorem drngring 20683

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ∖ cdif 3921  {csn 4599  ‘cfv 6528  Basecbs 17215  0_gc0g 17440  Ringcrg 20180  Unitcui 20302  DivRingcdr 20676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-iota 6481  df-fv 6536  df-drng 20678

This theorem is referenced by:  drngringd  20684  drngid  20693  drngunz  20694  drngnzr  20695  drngdomn  20696  drngmcl  20697  drnginvrcl  20700  drnginvrn0  20701  drnginvrl  20703  drnginvrr  20704  drngmul0orOLD  20708  drhmsubc  20728  drngcat  20729  sdrgid  20739  sdrgacs  20748  cntzsdrg  20749  primefld  20752  rlmlvec  21149  drngnidl  21191  drnglpir  21280  qsssubdrg  21381  frlmlvec  21708  frlmphllem  21727  mpllvec  21967  cvsdivcl  25071  qcvs  25086  cphsubrglem  25116  rrxcph  25331  rrx0  25336  drnguc1p  26118  ig1peu  26119  ig1pcl  26123  ig1pdvds  26124  ig1prsp  26125  ply1lpir  26126  padicabv  27579  ofldchr  33273  reofld  33296  rearchi  33298  xrge0slmod  33300  drng0mxidl  33428  drngmxidl  33429  zringfrac  33506  sradrng  33557  drgext0gsca  33566  drgextlsp  33568  rlmdim  33584  rgmoddimOLD  33585  frlmdim  33586  matdim  33590  drngdimgt0  33593  fedgmullem1  33604  fedgmullem2  33605  fedgmul  33606  fldextid  33636  extdg1id  33642  ccfldsrarelvec  33647  zrhunitpreima  33936  elzrhunit  33937  qqhval2lem  33941  qqh0  33944  qqh1  33945  qqhf  33946  qqhghm  33948  qqhrhm  33949  qqhnm  33950  qqhucn  33952  zrhre  33979  qqhre  33980  lindsdom  37567  lindsenlbs  37568  matunitlindflem1  37569  matunitlindflem2  37570  matunitlindf  37571  dvalveclem  40973  dvhlveclem  41056  hlhilsrnglem  41901  fldhmf1  42032  ricdrng1  42483  0prjspnrel  42582  drhmsubcALTV  48198  drngcatALTV  48199  aacllem  49506