Theorem drngring 20903

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ∖ cdif 3899  {csn 4587  ‘cfv 6537  Basecbs 17307  0_gc0g 17530  Ringcrg 20378  Unitcui 20502  DivRingcdr 20896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-drng 20898

This theorem is used by:  drngringd  20904  drngid  20915  drngunz  20916  drngnzr  20917  drngdomn  20918  drngmcl  20924  drnginvrcl  20926  drnginvrn0  20927  drnginvrl  20929  drnginvrr  20930  drhmsubc  20953  drngcat  20954  sdrgid  20964  sdrgacs  20973  cntzsdrg  20974  primefld  20977  rlmlvec  21394  drngnidl  21446  drnglpir  21569  qsssubdrg  21645  ofldchr  21795  frlmlvec  21980  frlmphllem  21999  lindsdom  22069  lindsenlbs  22070  mpllvec  22240  matunitlindflem1  22907  matunitlindflem2  22908  matunitlindf  22909  cvsdivcl  25367  qcvs  25381  cphsubrglem  25411  rrxcph  25626  rrx0  25631  drnguc1p  26406  ig1peu  26407  ig1pcl  26411  ig1pdvds  26412  ig1prsp  26413  ply1lpir  26414  padicabv  27874  reofld  33791  rearchi  33794  xrge0slmod  33796  drng0mxidl  33886  drngmxidl  33887  zringfrac  33972  sradrng  34100  drgext0gsca  34110  drgextlsp  34112  rlmdim  34128  frlmdim  34129  matdim  34133  drngdimgt0  34136  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  fldextid  34177  extdg1id  34184  ccfldsrarelvec  34189  zrhunitpreima  34494  elzrhunit  34495  qqhval2lem  34499  qqh0  34502  qqh1  34503  qqhf  34504  qqhghm  34506  qqhrhm  34507  qqhnm  34508  qqhucn  34510  zrhre  34537  qqhre  34538  dvalveclem  41906  dvhlveclem  41989  hlhilsrnglem  42834  fldhmf1  42964  ricdrng1  43418  0prjspnrel  43481  drhmsubcALTV  49252  drngcatALTV  49253  aacllem  50780  veroquadmodzerod  50825  veroquadnolindfd  50826