Theorem drngring 20314

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ∖ cdif 3944  {csn 4627  ‘cfv 6540  Basecbs 17140  0_gc0g 17381  Ringcrg 20049  Unitcui 20161  DivRingcdr 20307

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-drng 20309

This theorem is referenced by:  drngringd  20315  drngid  20325  drngunz  20326  drngnzr  20327  drnginvrcl  20329  drnginvrn0  20330  drnginvrl  20332  drnginvrr  20333  drngmul0or  20336  sdrgid  20400  sdrgacs  20409  cntzsdrg  20410  primefld  20413  abvtriv  20441  rlmlvec  20820  drngnidl  20846  drnglpir  20883  drngdomn  20913  qsssubdrg  20996  frlmlvec  21307  frlmphllem  21326  mpllvec  21570  cvsdivcl  24640  qcvs  24655  cphsubrglem  24685  rrxcph  24900  rrx0  24905  drnguc1p  25679  ig1peu  25680  ig1pcl  25684  ig1pdvds  25685  ig1prsp  25686  ply1lpir  25687  padicabv  27122  ofldchr  32420  reofld  32447  rearchi  32449  xrge0slmod  32451  drng0mxidl  32580  drngmxidl  32581  sradrng  32661  drgext0gsca  32667  drgextlsp  32669  rlmdim  32682  rgmoddimOLD  32683  frlmdim  32684  matdim  32688  drngdimgt0  32691  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  fldextid  32726  extdg1id  32730  ccfldsrarelvec  32733  zrhunitpreima  32946  elzrhunit  32947  qqhval2lem  32949  qqh0  32952  qqh1  32953  qqhf  32954  qqhghm  32956  qqhrhm  32957  qqhnm  32958  qqhucn  32960  zrhre  32987  qqhre  32988  lindsdom  36470  lindsenlbs  36471  matunitlindflem1  36472  matunitlindflem2  36473  matunitlindf  36474  dvalveclem  39884  dvhlveclem  39967  hlhilsrnglem  40816  fldhmf1  40943  ricdrng1  41099  0prjspnrel  41365  drhmsubc  46931  drngcat  46932  drhmsubcALTV  46949  drngcatALTV  46950  aacllem  47801