Theorem drngring 20007

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   ∖ cdif 3885  {csn 4562  ‘cfv 6437  Basecbs 16921  0_gc0g 17159  Ringcrg 19792  Unitcui 19890  DivRingcdr 20000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-drng 20002

This theorem is referenced by:  drnggrp  20008  drngid  20014  drngunz  20015  drnginvrcl  20017  drnginvrn0  20018  drnginvrl  20019  drnginvrr  20020  drngmul0or  20021  sdrgid  20073  sdrgacs  20078  cntzsdrg  20079  primefld  20082  abvtriv  20110  rlmlvec  20485  drngnidl  20509  drnglpir  20533  drngnzr  20542  drngdomn  20583  qsssubdrg  20666  frlmlvec  20977  frlmphllem  20996  frlmphl  20997  mpllvec  21234  cvsdivcl  24305  qcvs  24320  cphsubrglem  24350  rrxcph  24565  rrx0  24570  drnguc1p  25344  ig1peu  25345  ig1pcl  25349  ig1pdvds  25350  ig1prsp  25351  ply1lpir  25352  padicabv  26787  ofldchr  31522  reofld  31553  rearchi  31555  xrge0slmod  31557  sradrng  31682  drgext0gsca  31688  drgextlsp  31690  rgmoddim  31702  frlmdim  31703  matdim  31707  drngdimgt0  31710  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  fldextid  31743  extdg1id  31747  ccfldsrarelvec  31750  zrhunitpreima  31937  elzrhunit  31938  qqhval2lem  31940  qqh0  31943  qqh1  31944  qqhf  31945  qqhghm  31947  qqhrhm  31948  qqhnm  31949  qqhucn  31951  zrhre  31978  qqhre  31979  lindsdom  35780  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  matunitlindf  35784  dvalveclem  39046  dvhlveclem  39129  hlhilsrnglem  39978  drngringd  40253  0prjspnrel  40471  drhmsubc  45649  drngcat  45650  drhmsubcALTV  45667  drngcatALTV  45668  aacllem  46516