Theorem drngring 21017

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ∖ cdif 4048  {csn 4588  ‘cfv 6558  Basecbs 17416  0_gc0g 17639  Ringcrg 20489  Unitcui 20615  DivRingcdr 21010

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-drng 21012

This theorem is used by:  drngringd  21018  drngid  21030  drngunz  21031  drngnzr  21032  drngdomn  21033  drngmcl  21039  drnginvrcl  21041  drnginvrn0  21042  drnginvrl  21044  drnginvrr  21045  drhmsubc  21068  drngcat  21069  sdrgid  21079  sdrgacs  21088  cntzsdrg  21089  primefld  21092  rlmlvec  21509  drngnidl  21561  drnglpir  21686  qsssubdrg  21762  ofldchr  21912  frlmlvec  22097  frlmphllem  22116  lindsdom  22186  lindsenlbs  22187  mpllvec  22357  matunitlindflem1  23024  matunitlindflem2  23025  matunitlindf  23026  cvsdivcl  25484  qcvs  25498  cphsubrglem  25528  rrxcph  25743  rrx0  25748  drnguc1p  26522  ig1peu  26523  ig1pcl  26527  ig1pdvds  26528  ig1prsp  26529  ply1lpir  26530  padicabv  27987  reofld  33974  rearchi  33977  xrge0slmod  33979  drng0mxidl  34070  drngmxidl  34071  zringfrac  34156  sradrng  34284  drgext0gsca  34294  drgextlsp  34296  rlmdim  34312  frlmdim  34313  matdim  34317  drngdimgt0  34320  fedgmullem1  34331  fedgmullem2  34332  fldextid  34361  extdg1id  34368  ccfldsrarelvec  34373  zrhunitpreima  34678  elzrhunit  34679  qqhval2lem  34683  qqh0  34686  qqh1  34687  qqhf  34688  qqhghm  34690  qqhrhm  34691  qqhnm  34692  qqhucn  34694  zrhre  34721  qqhre  34722  dvalveclem  42274  dvhlveclem  42357  hlhilsrnglem  43202  fldhmf1  43332  ricdrng1  43785  0prjspnrel  43856  drhmsubcALTV  49631  drngcatALTV  49632  aacllem  51219  veroquadmodzerod  51264  veroquadnolindfd  51265