Theorem drngring 20645

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ∖ cdif 3946  {csn 4632  ‘cfv 6553  Basecbs 17189  0_gc0g 17430  Ringcrg 20187  Unitcui 20308  DivRingcdr 20638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-iota 6505  df-fv 6561  df-drng 20640

This theorem is referenced by:  drngringd  20646  drngid  20656  drngunz  20657  drngnzr  20658  drnginvrcl  20660  drnginvrn0  20661  drnginvrl  20663  drnginvrr  20664  drngmul0or  20667  drhmsubc  20683  drngcat  20684  sdrgid  20694  sdrgacs  20703  cntzsdrg  20704  primefld  20707  abvtriv  20735  rlmlvec  21111  drngnidl  21152  drnglpir  21236  drngdomn  21267  qsssubdrg  21373  frlmlvec  21709  frlmphllem  21728  mpllvec  21979  cvsdivcl  25088  qcvs  25103  cphsubrglem  25133  rrxcph  25348  rrx0  25353  drnguc1p  26136  ig1peu  26137  ig1pcl  26141  ig1pdvds  26142  ig1prsp  26143  ply1lpir  26144  padicabv  27591  ofldchr  33061  reofld  33088  rearchi  33090  xrge0slmod  33092  drng0mxidl  33222  drngmxidl  33223  zringfrac  33285  sradrng  33324  drgext0gsca  33332  drgextlsp  33334  rlmdim  33348  rgmoddimOLD  33349  frlmdim  33350  matdim  33354  drngdimgt0  33357  fedgmullem1  33368  fedgmullem2  33369  fedgmul  33370  fldextid  33392  extdg1id  33396  ccfldsrarelvec  33400  zrhunitpreima  33620  elzrhunit  33621  qqhval2lem  33623  qqh0  33626  qqh1  33627  qqhf  33628  qqhghm  33630  qqhrhm  33631  qqhnm  33632  qqhucn  33634  zrhre  33661  qqhre  33662  lindsdom  37128  lindsenlbs  37129  matunitlindflem1  37130  matunitlindflem2  37131  matunitlindf  37132  dvalveclem  40538  dvhlveclem  40621  hlhilsrnglem  41470  fldhmf1  41601  ricdrng1  41804  0prjspnrel  42100  drhmsubcALTV  47487  drngcatALTV  47488  aacllem  48330