Theorem drngring 20507

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   ∖ cdif 3944  {csn 4627  ‘cfv 6542  Basecbs 17148  0_gc0g 17389  Ringcrg 20127  Unitcui 20246  DivRingcdr 20500

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-drng 20502

This theorem is referenced by:  drngringd  20508  drngid  20518  drngunz  20519  drngnzr  20520  drnginvrcl  20522  drnginvrn0  20523  drnginvrl  20525  drnginvrr  20526  drngmul0or  20529  sdrgid  20551  sdrgacs  20560  cntzsdrg  20561  primefld  20564  abvtriv  20592  rlmlvec  20973  drngnidl  21003  drnglpir  21091  drngdomn  21121  qsssubdrg  21204  frlmlvec  21535  frlmphllem  21554  mpllvec  21798  cvsdivcl  24880  qcvs  24895  cphsubrglem  24925  rrxcph  25140  rrx0  25145  drnguc1p  25923  ig1peu  25924  ig1pcl  25928  ig1pdvds  25929  ig1prsp  25930  ply1lpir  25931  padicabv  27369  ofldchr  32702  reofld  32729  rearchi  32731  xrge0slmod  32733  drng0mxidl  32866  drngmxidl  32867  sradrng  32958  drgext0gsca  32966  drgextlsp  32968  rlmdim  32982  rgmoddimOLD  32983  frlmdim  32984  matdim  32988  drngdimgt0  32991  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  fldextid  33026  extdg1id  33030  ccfldsrarelvec  33034  zrhunitpreima  33256  elzrhunit  33257  qqhval2lem  33259  qqh0  33262  qqh1  33263  qqhf  33264  qqhghm  33266  qqhrhm  33267  qqhnm  33268  qqhucn  33270  zrhre  33297  qqhre  33298  lindsdom  36785  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  matunitlindf  36789  dvalveclem  40199  dvhlveclem  40282  hlhilsrnglem  41131  fldhmf1  41261  ricdrng1  41406  0prjspnrel  41671  drhmsubc  47066  drngcat  47067  drhmsubcALTV  47084  drngcatALTV  47085  aacllem  47935