Theorem drngring 20992

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ∖ cdif 4045  {csn 4584  ‘cfv 6538  Basecbs 17392  0_gc0g 17615  Ringcrg 20464  Unitcui 20590  DivRingcdr 20985

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-drng 20987

This theorem is used by:  drngringd  20993  drngid  21005  drngunz  21006  drngnzr  21007  drngdomn  21008  drngmcl  21014  drnginvrcl  21016  drnginvrn0  21017  drnginvrl  21019  drnginvrr  21020  drhmsubc  21043  drngcat  21044  sdrgid  21054  sdrgacs  21063  cntzsdrg  21064  primefld  21067  rlmlvec  21484  drngnidl  21536  drnglpir  21661  qsssubdrg  21737  ofldchr  21887  frlmlvec  22072  frlmphllem  22091  lindsdom  22161  lindsenlbs  22162  mpllvec  22332  matunitlindflem1  22999  matunitlindflem2  23000  matunitlindf  23001  cvsdivcl  25459  qcvs  25473  cphsubrglem  25503  rrxcph  25718  rrx0  25723  drnguc1p  26497  ig1peu  26498  ig1pcl  26502  ig1pdvds  26503  ig1prsp  26504  ply1lpir  26505  padicabv  27962  reofld  33950  rearchi  33953  xrge0slmod  33955  drng0mxidl  34046  drngmxidl  34047  zringfrac  34132  sradrng  34260  drgext0gsca  34270  drgextlsp  34272  rlmdim  34288  frlmdim  34289  matdim  34293  drngdimgt0  34296  fedgmullem1  34307  fedgmullem2  34308  fldextid  34337  extdg1id  34344  ccfldsrarelvec  34349  zrhunitpreima  34654  elzrhunit  34655  qqhval2lem  34659  qqh0  34662  qqh1  34663  qqhf  34664  qqhghm  34666  qqhrhm  34667  qqhnm  34668  qqhucn  34670  zrhre  34697  qqhre  34698  dvalveclem  42175  dvhlveclem  42258  hlhilsrnglem  43103  fldhmf1  43233  ricdrng1  43685  0prjspnrel  43756  drhmsubcALTV  49519  drngcatALTV  49520  aacllem  51107  veroquadmodzerod  51152  veroquadnolindfd  51153