Theorem drngring 20681

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3900  {csn 4582  ‘cfv 6500  Basecbs 17148  0_gc0g 17371  Ringcrg 20180  Unitcui 20303  DivRingcdr 20674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-drng 20676

This theorem is referenced by:  drngringd  20682  drngid  20691  drngunz  20692  drngnzr  20693  drngdomn  20694  drngmcl  20695  drnginvrcl  20698  drnginvrn0  20699  drnginvrl  20701  drnginvrr  20702  drngmul0orOLD  20706  drhmsubc  20726  drngcat  20727  sdrgid  20737  sdrgacs  20746  cntzsdrg  20747  primefld  20750  rlmlvec  21168  drngnidl  21210  drnglpir  21299  qsssubdrg  21393  ofldchr  21543  frlmlvec  21728  frlmphllem  21747  mpllvec  21987  cvsdivcl  25101  qcvs  25115  cphsubrglem  25145  rrxcph  25360  rrx0  25365  drnguc1p  26147  ig1peu  26148  ig1pcl  26152  ig1pdvds  26153  ig1prsp  26154  ply1lpir  26155  padicabv  27609  reofld  33435  rearchi  33438  xrge0slmod  33440  drng0mxidl  33568  drngmxidl  33569  zringfrac  33646  sradrng  33758  drgext0gsca  33768  drgextlsp  33770  rlmdim  33786  rgmoddimOLD  33787  frlmdim  33788  matdim  33792  drngdimgt0  33795  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  fldextid  33836  extdg1id  33843  ccfldsrarelvec  33848  zrhunitpreima  34153  elzrhunit  34154  qqhval2lem  34158  qqh0  34161  qqh1  34162  qqhf  34163  qqhghm  34165  qqhrhm  34166  qqhnm  34167  qqhucn  34169  zrhre  34196  qqhre  34197  lindsdom  37859  lindsenlbs  37860  matunitlindflem1  37861  matunitlindflem2  37862  matunitlindf  37863  dvalveclem  41395  dvhlveclem  41478  hlhilsrnglem  42323  fldhmf1  42454  ricdrng1  42892  0prjspnrel  42979  drhmsubcALTV  48683  drngcatALTV  48684  aacllem  50154