Theorem drngring 20967

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 2761	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2761	. . 3 ⊢ (Unit‘𝑅) = (Unit‘𝑅)
3		eqid 2761	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
4	1, 2, 3	isdrng 20964	. 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 3896  {csn 4584  ‘cfv 6531  Basecbs 17367  0_gc0g 17590  Ringcrg 20439  Unitcui 20565  DivRingcdr 20960

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-drng 20962

This theorem is used by:  drngringd  20968  drngid  20980  drngunz  20981  drngnzr  20982  drngdomn  20983  drngmcl  20989  drnginvrcl  20991  drnginvrn0  20992  drnginvrl  20994  drnginvrr  20995  drhmsubc  21018  drngcat  21019  sdrgid  21029  sdrgacs  21038  cntzsdrg  21039  primefld  21042  rlmlvec  21459  drngnidl  21511  drnglpir  21636  qsssubdrg  21712  ofldchr  21862  frlmlvec  22047  frlmphllem  22066  lindsdom  22136  lindsenlbs  22137  mpllvec  22307  matunitlindflem1  22974  matunitlindflem2  22975  matunitlindf  22976  cvsdivcl  25434  qcvs  25448  cphsubrglem  25478  rrxcph  25693  rrx0  25698  drnguc1p  26472  ig1peu  26473  ig1pcl  26477  ig1pdvds  26478  ig1prsp  26479  ply1lpir  26480  padicabv  27939  reofld  33886  rearchi  33889  xrge0slmod  33891  drng0mxidl  33982  drngmxidl  33983  zringfrac  34068  sradrng  34196  drgext0gsca  34206  drgextlsp  34208  rlmdim  34224  frlmdim  34225  matdim  34229  drngdimgt0  34232  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  fldextid  34273  extdg1id  34280  ccfldsrarelvec  34285  zrhunitpreima  34590  elzrhunit  34591  qqhval2lem  34595  qqh0  34598  qqh1  34599  qqhf  34600  qqhghm  34602  qqhrhm  34603  qqhnm  34604  qqhucn  34606  zrhre  34633  qqhre  34634  dvalveclem  42050  dvhlveclem  42133  hlhilsrnglem  42978  fldhmf1  43108  ricdrng1  43554  0prjspnrel  43617  drhmsubcALTV  49370  drngcatALTV  49371  aacllem  50883  veroquadmodzerod  50928  veroquadnolindfd  50929