Theorem drngring 20821

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 20818	. 2 ⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g‘𝑅)})))
5	4	simplbi 501	1 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   ∖ cdif 3903  {csn 4590  ‘cfv 6538  Basecbs 17270  0_gc0g 17493  Ringcrg 20316  Unitcui 20438  DivRingcdr 20814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-drng 20816

This theorem is referenced by:  drngringd  20822  drngid  20833  drngunz  20834  drngnzr  20835  drngdomn  20836  drngmcl  20837  drnginvrcl  20839  drnginvrn0  20840  drnginvrl  20842  drnginvrr  20843  drhmsubc  20865  drngcat  20866  sdrgid  20876  sdrgacs  20885  cntzsdrg  20886  primefld  20889  rlmlvec  21306  drngnidl  21358  drnglpir  21481  qsssubdrg  21557  ofldchr  21707  frlmlvec  21892  frlmphllem  21911  mpllvec  22150  cvsdivcl  25273  qcvs  25287  cphsubrglem  25317  rrxcph  25532  rrx0  25537  drnguc1p  26312  ig1peu  26313  ig1pcl  26317  ig1pdvds  26318  ig1prsp  26319  ply1lpir  26320  padicabv  27772  reofld  33641  rearchi  33644  xrge0slmod  33646  drng0mxidl  33736  drngmxidl  33737  zringfrac  33822  sradrng  33950  drgext0gsca  33960  drgextlsp  33962  rlmdim  33978  frlmdim  33979  matdim  33983  drngdimgt0  33986  fedgmullem1  33997  fedgmullem2  33998  fedgmul  33999  fldextid  34027  extdg1id  34034  ccfldsrarelvec  34039  zrhunitpreima  34344  elzrhunit  34345  qqhval2lem  34349  qqh0  34352  qqh1  34353  qqhf  34354  qqhghm  34356  qqhrhm  34357  qqhnm  34358  qqhucn  34360  zrhre  34387  qqhre  34388  lindsdom  38243  lindsenlbs  38244  matunitlindflem1  38245  matunitlindflem2  38246  matunitlindf  38247  dvalveclem  41777  dvhlveclem  41860  hlhilsrnglem  42705  fldhmf1  42835  ricdrng1  43276  0prjspnrel  43339  drhmsubcALTV  49071  drngcatALTV  49072  aacllem  50578