Theorem drngring 19913

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ∖ cdif 3880  {csn 4558  ‘cfv 6418  Basecbs 16840  0_gc0g 17067  Ringcrg 19698  Unitcui 19796  DivRingcdr 19906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-drng 19908

This theorem is referenced by:  drnggrp  19914  drngid  19920  drngunz  19921  drnginvrcl  19923  drnginvrn0  19924  drnginvrl  19925  drnginvrr  19926  drngmul0or  19927  sdrgid  19979  sdrgacs  19984  cntzsdrg  19985  primefld  19988  abvtriv  20016  rlmlvec  20389  drngnidl  20413  drnglpir  20437  drngnzr  20446  drngdomn  20487  qsssubdrg  20569  frlmlvec  20878  frlmphllem  20897  frlmphl  20898  mpllvec  21135  cvsdivcl  24202  qcvs  24216  cphsubrglem  24246  rrxcph  24461  rrx0  24466  drnguc1p  25240  ig1peu  25241  ig1pcl  25245  ig1pdvds  25246  ig1prsp  25247  ply1lpir  25248  padicabv  26683  ofldchr  31415  reofld  31446  rearchi  31448  xrge0slmod  31450  sradrng  31575  drgext0gsca  31581  drgextlsp  31583  rgmoddim  31595  frlmdim  31596  matdim  31600  drngdimgt0  31603  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  fldextid  31636  extdg1id  31640  ccfldsrarelvec  31643  zrhunitpreima  31828  elzrhunit  31829  qqhval2lem  31831  qqh0  31834  qqh1  31835  qqhf  31836  qqhghm  31838  qqhrhm  31839  qqhnm  31840  qqhucn  31842  zrhre  31869  qqhre  31870  lindsdom  35698  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  matunitlindf  35702  dvalveclem  38966  dvhlveclem  39049  hlhilsrnglem  39898  drngringd  40172  0prjspnrel  40385  drhmsubc  45526  drngcat  45527  drhmsubcALTV  45544  drngcatALTV  45545  aacllem  46391