Theorem drngring 20752

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ∖ cdif 3959  {csn 4630  ‘cfv 6562  Basecbs 17244  0_gc0g 17485  Ringcrg 20250  Unitcui 20371  DivRingcdr 20745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-drng 20747

This theorem is referenced by:  drngringd  20753  drngid  20762  drngunz  20763  drngnzr  20764  drngdomn  20765  drngmcl  20766  drnginvrcl  20769  drnginvrn0  20770  drnginvrl  20772  drnginvrr  20773  drngmul0orOLD  20777  drhmsubc  20798  drngcat  20799  sdrgid  20809  sdrgacs  20818  cntzsdrg  20819  primefld  20822  rlmlvec  21228  drngnidl  21270  drnglpir  21359  qsssubdrg  21461  frlmlvec  21798  frlmphllem  21817  mpllvec  22057  cvsdivcl  25179  qcvs  25194  cphsubrglem  25224  rrxcph  25439  rrx0  25444  drnguc1p  26227  ig1peu  26228  ig1pcl  26232  ig1pdvds  26233  ig1prsp  26234  ply1lpir  26235  padicabv  27688  ofldchr  33323  reofld  33351  rearchi  33353  xrge0slmod  33355  drng0mxidl  33483  drngmxidl  33484  zringfrac  33561  sradrng  33612  drgext0gsca  33620  drgextlsp  33622  rlmdim  33636  rgmoddimOLD  33637  frlmdim  33638  matdim  33642  drngdimgt0  33645  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  fldextid  33686  extdg1id  33690  ccfldsrarelvec  33695  zrhunitpreima  33938  elzrhunit  33939  qqhval2lem  33943  qqh0  33946  qqh1  33947  qqhf  33948  qqhghm  33950  qqhrhm  33951  qqhnm  33952  qqhucn  33954  zrhre  33981  qqhre  33982  lindsdom  37600  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  dvalveclem  41007  dvhlveclem  41090  hlhilsrnglem  41939  fldhmf1  42071  ricdrng1  42514  0prjspnrel  42613  drhmsubcALTV  48172  drngcatALTV  48173  aacllem  49031