Theorem drngring 20594

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ∖ cdif 3940  {csn 4623  ‘cfv 6537  Basecbs 17153  0_gc0g 17394  Ringcrg 20138  Unitcui 20257  DivRingcdr 20587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6489  df-fv 6545  df-drng 20589

This theorem is referenced by:  drngringd  20595  drngid  20605  drngunz  20606  drngnzr  20607  drnginvrcl  20609  drnginvrn0  20610  drnginvrl  20612  drnginvrr  20613  drngmul0or  20616  drhmsubc  20632  drngcat  20633  sdrgid  20643  sdrgacs  20652  cntzsdrg  20653  primefld  20656  abvtriv  20684  rlmlvec  21060  drngnidl  21101  drnglpir  21185  drngdomn  21215  qsssubdrg  21320  frlmlvec  21656  frlmphllem  21675  mpllvec  21921  cvsdivcl  25015  qcvs  25030  cphsubrglem  25060  rrxcph  25275  rrx0  25280  drnguc1p  26063  ig1peu  26064  ig1pcl  26068  ig1pdvds  26069  ig1prsp  26070  ply1lpir  26071  padicabv  27518  ofldchr  32935  reofld  32962  rearchi  32964  xrge0slmod  32966  drng0mxidl  33098  drngmxidl  33099  sradrng  33188  drgext0gsca  33196  drgextlsp  33198  rlmdim  33212  rgmoddimOLD  33213  frlmdim  33214  matdim  33218  drngdimgt0  33221  fedgmullem1  33232  fedgmullem2  33233  fedgmul  33234  fldextid  33256  extdg1id  33260  ccfldsrarelvec  33264  zrhunitpreima  33488  elzrhunit  33489  qqhval2lem  33491  qqh0  33494  qqh1  33495  qqhf  33496  qqhghm  33498  qqhrhm  33499  qqhnm  33500  qqhucn  33502  zrhre  33529  qqhre  33530  lindsdom  36995  lindsenlbs  36996  matunitlindflem1  36997  matunitlindflem2  36998  matunitlindf  36999  dvalveclem  40409  dvhlveclem  40492  hlhilsrnglem  41341  fldhmf1  41471  ricdrng1  41658  0prjspnrel  41944  drhmsubcALTV  47276  drngcatALTV  47277  aacllem  48119