Theorem drngring 19502

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ∖ cdif 3878  {csn 4525  ‘cfv 6324  Basecbs 16475  0_gc0g 16705  Ringcrg 19290  Unitcui 19385  DivRingcdr 19495

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-drng 19497

This theorem is referenced by:  drnggrp  19503  drngid  19509  drngunz  19510  drnginvrcl  19512  drnginvrn0  19513  drnginvrl  19514  drnginvrr  19515  drngmul0or  19516  sdrgid  19568  sdrgacs  19573  cntzsdrg  19574  primefld  19577  abvtriv  19605  rlmlvec  19971  drngnidl  19995  drnglpir  20019  drngnzr  20028  drngdomn  20069  qsssubdrg  20150  frlmlvec  20450  frlmphllem  20469  frlmphl  20470  mpllvec  20692  cvsdivcl  23738  qcvs  23752  cphsubrglem  23782  rrxcph  23996  rrx0  24001  drnguc1p  24771  ig1peu  24772  ig1pcl  24776  ig1pdvds  24777  ig1prsp  24778  ply1lpir  24779  padicabv  26214  ofldchr  30938  reofld  30964  rearchi  30966  xrge0slmod  30968  sradrng  31076  drgext0gsca  31082  drgextlsp  31084  rgmoddim  31096  frlmdim  31097  matdim  31101  drngdimgt0  31104  fedgmullem1  31113  fedgmullem2  31114  fedgmul  31115  fldextid  31137  extdg1id  31141  ccfldsrarelvec  31144  zrhunitpreima  31329  elzrhunit  31330  qqhval2lem  31332  qqh0  31335  qqh1  31336  qqhf  31337  qqhghm  31339  qqhrhm  31340  qqhnm  31341  qqhucn  31343  zrhre  31370  qqhre  31371  lindsdom  35051  lindsenlbs  35052  matunitlindflem1  35053  matunitlindflem2  35054  matunitlindf  35055  dvalveclem  38321  dvhlveclem  38404  hlhilsrnglem  39249  drngringd  39445  0prjspnrel  39613  drhmsubc  44704  drngcat  44705  drhmsubcALTV  44722  drngcatALTV  44723  aacllem  45329