Theorem drngring 20652

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∖ cdif 3914  {csn 4592  ‘cfv 6514  Basecbs 17186  0_gc0g 17409  Ringcrg 20149  Unitcui 20271  DivRingcdr 20645

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-drng 20647

This theorem is referenced by:  drngringd  20653  drngid  20662  drngunz  20663  drngnzr  20664  drngdomn  20665  drngmcl  20666  drnginvrcl  20669  drnginvrn0  20670  drnginvrl  20672  drnginvrr  20673  drngmul0orOLD  20677  drhmsubc  20697  drngcat  20698  sdrgid  20708  sdrgacs  20717  cntzsdrg  20718  primefld  20721  rlmlvec  21118  drngnidl  21160  drnglpir  21249  qsssubdrg  21350  frlmlvec  21677  frlmphllem  21696  mpllvec  21936  cvsdivcl  25040  qcvs  25054  cphsubrglem  25084  rrxcph  25299  rrx0  25304  drnguc1p  26086  ig1peu  26087  ig1pcl  26091  ig1pdvds  26092  ig1prsp  26093  ply1lpir  26094  padicabv  27548  ofldchr  33299  reofld  33322  rearchi  33324  xrge0slmod  33326  drng0mxidl  33454  drngmxidl  33455  zringfrac  33532  sradrng  33585  drgext0gsca  33594  drgextlsp  33596  rlmdim  33612  rgmoddimOLD  33613  frlmdim  33614  matdim  33618  drngdimgt0  33621  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  fldextid  33662  extdg1id  33668  ccfldsrarelvec  33673  zrhunitpreima  33973  elzrhunit  33974  qqhval2lem  33978  qqh0  33981  qqh1  33982  qqhf  33983  qqhghm  33985  qqhrhm  33986  qqhnm  33987  qqhucn  33989  zrhre  34016  qqhre  34017  lindsdom  37615  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  matunitlindf  37619  dvalveclem  41026  dvhlveclem  41109  hlhilsrnglem  41954  fldhmf1  42085  ricdrng1  42523  0prjspnrel  42622  drhmsubcALTV  48321  drngcatALTV  48322  aacllem  49794