Theorem drngring 20696

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∖ cdif 3923  {csn 4601  ‘cfv 6531  Basecbs 17228  0_gc0g 17453  Ringcrg 20193  Unitcui 20315  DivRingcdr 20689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-drng 20691

This theorem is referenced by:  drngringd  20697  drngid  20706  drngunz  20707  drngnzr  20708  drngdomn  20709  drngmcl  20710  drnginvrcl  20713  drnginvrn0  20714  drnginvrl  20716  drnginvrr  20717  drngmul0orOLD  20721  drhmsubc  20741  drngcat  20742  sdrgid  20752  sdrgacs  20761  cntzsdrg  20762  primefld  20765  rlmlvec  21162  drngnidl  21204  drnglpir  21293  qsssubdrg  21394  frlmlvec  21721  frlmphllem  21740  mpllvec  21980  cvsdivcl  25084  qcvs  25099  cphsubrglem  25129  rrxcph  25344  rrx0  25349  drnguc1p  26131  ig1peu  26132  ig1pcl  26136  ig1pdvds  26137  ig1prsp  26138  ply1lpir  26139  padicabv  27593  ofldchr  33336  reofld  33359  rearchi  33361  xrge0slmod  33363  drng0mxidl  33491  drngmxidl  33492  zringfrac  33569  sradrng  33622  drgext0gsca  33631  drgextlsp  33633  rlmdim  33649  rgmoddimOLD  33650  frlmdim  33651  matdim  33655  drngdimgt0  33658  fedgmullem1  33669  fedgmullem2  33670  fedgmul  33671  fldextid  33701  extdg1id  33707  ccfldsrarelvec  33712  zrhunitpreima  34007  elzrhunit  34008  qqhval2lem  34012  qqh0  34015  qqh1  34016  qqhf  34017  qqhghm  34019  qqhrhm  34020  qqhnm  34021  qqhucn  34023  zrhre  34050  qqhre  34051  lindsdom  37638  lindsenlbs  37639  matunitlindflem1  37640  matunitlindflem2  37641  matunitlindf  37642  dvalveclem  41044  dvhlveclem  41127  hlhilsrnglem  41972  fldhmf1  42103  ricdrng1  42551  0prjspnrel  42650  drhmsubcALTV  48304  drngcatALTV  48305  aacllem  49665