Theorem drngring 20704

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3887  {csn 4568  ‘cfv 6492  Basecbs 17170  0_gc0g 17393  Ringcrg 20205  Unitcui 20326  DivRingcdr 20697

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-drng 20699

This theorem is referenced by:  drngringd  20705  drngid  20714  drngunz  20715  drngnzr  20716  drngdomn  20717  drngmcl  20718  drnginvrcl  20721  drnginvrn0  20722  drnginvrl  20724  drnginvrr  20725  drngmul0orOLD  20729  drhmsubc  20749  drngcat  20750  sdrgid  20760  sdrgacs  20769  cntzsdrg  20770  primefld  20773  rlmlvec  21191  drngnidl  21233  drnglpir  21322  qsssubdrg  21416  ofldchr  21566  frlmlvec  21751  frlmphllem  21770  mpllvec  22008  cvsdivcl  25110  qcvs  25124  cphsubrglem  25154  rrxcph  25369  rrx0  25374  drnguc1p  26149  ig1peu  26150  ig1pcl  26154  ig1pdvds  26155  ig1prsp  26156  ply1lpir  26157  padicabv  27607  reofld  33418  rearchi  33421  xrge0slmod  33423  drng0mxidl  33551  drngmxidl  33552  zringfrac  33629  sradrng  33741  drgext0gsca  33751  drgextlsp  33753  rlmdim  33769  rgmoddimOLD  33770  frlmdim  33771  matdim  33775  drngdimgt0  33778  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  fldextid  33819  extdg1id  33826  ccfldsrarelvec  33831  zrhunitpreima  34136  elzrhunit  34137  qqhval2lem  34141  qqh0  34144  qqh1  34145  qqhf  34146  qqhghm  34148  qqhrhm  34149  qqhnm  34150  qqhucn  34152  zrhre  34179  qqhre  34180  lindsdom  37949  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  matunitlindf  37953  dvalveclem  41485  dvhlveclem  41568  hlhilsrnglem  42413  fldhmf1  42543  ricdrng1  42987  0prjspnrel  43074  drhmsubcALTV  48817  drngcatALTV  48818  aacllem  50288