Theorem drngring 19590

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ∖ cdif 3857  {csn 4525  ‘cfv 6340  Basecbs 16554  0_gc0g 16784  Ringcrg 19378  Unitcui 19473  DivRingcdr 19583

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 2729

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 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-drng 19585

This theorem is referenced by:  drnggrp  19591  drngid  19597  drngunz  19598  drnginvrcl  19600  drnginvrn0  19601  drnginvrl  19602  drnginvrr  19603  drngmul0or  19604  sdrgid  19656  sdrgacs  19661  cntzsdrg  19662  primefld  19665  abvtriv  19693  rlmlvec  20059  drngnidl  20083  drnglpir  20107  drngnzr  20116  drngdomn  20157  qsssubdrg  20238  frlmlvec  20539  frlmphllem  20558  frlmphl  20559  mpllvec  20797  cvsdivcl  23847  qcvs  23861  cphsubrglem  23891  rrxcph  24105  rrx0  24110  drnguc1p  24883  ig1peu  24884  ig1pcl  24888  ig1pdvds  24889  ig1prsp  24890  ply1lpir  24891  padicabv  26326  ofldchr  31051  reofld  31077  rearchi  31079  xrge0slmod  31081  sradrng  31206  drgext0gsca  31212  drgextlsp  31214  rgmoddim  31226  frlmdim  31227  matdim  31231  drngdimgt0  31234  fedgmullem1  31243  fedgmullem2  31244  fedgmul  31245  fldextid  31267  extdg1id  31271  ccfldsrarelvec  31274  zrhunitpreima  31459  elzrhunit  31460  qqhval2lem  31462  qqh0  31465  qqh1  31466  qqhf  31467  qqhghm  31469  qqhrhm  31470  qqhnm  31471  qqhucn  31473  zrhre  31500  qqhre  31501  lindsdom  35365  lindsenlbs  35366  matunitlindflem1  35367  matunitlindflem2  35368  matunitlindf  35369  dvalveclem  38635  dvhlveclem  38718  hlhilsrnglem  39563  drngringd  39789  0prjspnrel  39996  drhmsubc  45120  drngcat  45121  drhmsubcALTV  45138  drngcatALTV  45139  aacllem  45814