Theorem drngring 20811

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145   ∖ cdif 3904  {csn 4585  ‘cfv 6525  Basecbs 17259  0_gc0g 17482  Ringcrg 20306  Unitcui 20428  DivRingcdr 20804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-drng 20806

This theorem is referenced by:  drngringd  20812  drngid  20821  drngunz  20822  drngnzr  20823  drngdomn  20824  drngmcl  20825  drnginvrcl  20827  drnginvrn0  20828  drnginvrl  20830  drnginvrr  20831  drhmsubc  20853  drngcat  20854  sdrgid  20864  sdrgacs  20873  cntzsdrg  20874  primefld  20877  rlmlvec  21294  drngnidl  21342  drnglpir  21460  qsssubdrg  21536  ofldchr  21686  frlmlvec  21871  frlmphllem  21890  mpllvec  22129  cvsdivcl  25253  qcvs  25267  cphsubrglem  25297  rrxcph  25512  rrx0  25517  drnguc1p  26292  ig1peu  26293  ig1pcl  26297  ig1pdvds  26298  ig1prsp  26299  ply1lpir  26300  padicabv  27752  reofld  33578  rearchi  33581  xrge0slmod  33583  drng0mxidl  33675  drngmxidl  33676  zringfrac  33761  sradrng  33889  drgext0gsca  33899  drgextlsp  33901  rlmdim  33917  frlmdim  33918  matdim  33922  drngdimgt0  33925  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  fldextid  33966  extdg1id  33973  ccfldsrarelvec  33978  zrhunitpreima  34283  elzrhunit  34284  qqhval2lem  34288  qqh0  34291  qqh1  34292  qqhf  34293  qqhghm  34295  qqhrhm  34296  qqhnm  34297  qqhucn  34299  zrhre  34326  qqhre  34327  lindsdom  38125  lindsenlbs  38126  matunitlindflem1  38127  matunitlindflem2  38128  matunitlindf  38129  dvalveclem  41661  dvhlveclem  41744  hlhilsrnglem  42589  fldhmf1  42719  ricdrng1  43158  0prjspnrel  43221  drhmsubcALTV  48949  drngcatALTV  48950  aacllem  50430