Theorem drngring 18963

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

Syntax hints:   → wi 4   = wceq 1630   ∈ wcel 2144   ∖ cdif 3718  {csn 4314  ‘cfv 6031  Basecbs 16063  0_gc0g 16307  Ringcrg 18754  Unitcui 18846  DivRingcdr 18956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-drng 18958

This theorem is referenced by:  drnggrp  18964  drngid  18970  drngunz  18971  drnginvrcl  18973  drnginvrn0  18974  drnginvrl  18975  drnginvrr  18976  drngmul0or  18977  abvtriv  19050  rlmlvec  19420  drngnidl  19443  drnglpir  19467  drngnzr  19476  drngdomn  19517  qsssubdrg  20019  frlmphllem  20335  frlmphl  20336  cvsdivcl  23151  qcvs  23165  cphsubrglem  23195  rrxcph  23398  drnguc1p  24149  ig1peu  24150  ig1pcl  24154  ig1pdvds  24155  ig1prsp  24156  ply1lpir  24157  padicabv  25539  ofldchr  30148  reofld  30174  rearchi  30176  xrge0slmod  30178  zrhunitpreima  30356  elzrhunit  30357  qqhval2lem  30359  qqh0  30362  qqh1  30363  qqhf  30364  qqhghm  30366  qqhrhm  30367  qqhnm  30368  qqhucn  30370  zrhre  30397  qqhre  30398  lindsdom  33729  lindsenlbs  33730  matunitlindflem1  33731  matunitlindflem2  33732  matunitlindf  33733  dvalveclem  36828  dvhlveclem  36911  hlhilsrnglem  37756  sdrgacs  38290  cntzsdrg  38291  drhmsubc  42598  drngcat  42599  drhmsubcALTV  42616  drngcatALTV  42617  aacllem  43068