MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  drngring Structured version   Visualization version   GIF version

Theorem drngring 18965
Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
Assertion
Ref Expression
drngring (𝑅 ∈ DivRing → 𝑅 ∈ Ring)

Proof of Theorem drngring
StepHypRef Expression
1 eqid 2817 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2817 . . 3 (Unit‘𝑅) = (Unit‘𝑅)
3 eqid 2817 . . 3 (0g𝑅) = (0g𝑅)
41, 2, 3isdrng 18962 . 2 (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ (Unit‘𝑅) = ((Base‘𝑅) ∖ {(0g𝑅)})))
54simplbi 487 1 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  cdif 3777  {csn 4381  cfv 6108  Basecbs 16075  0gc0g 16312  Ringcrg 18756  Unitcui 18848  DivRingcdr 18958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6071  df-fv 6116  df-drng 18960
This theorem is referenced by:  drnggrp  18966  drngid  18972  drngunz  18973  drnginvrcl  18975  drnginvrn0  18976  drnginvrl  18977  drnginvrr  18978  drngmul0or  18979  abvtriv  19052  rlmlvec  19422  drngnidl  19445  drnglpir  19469  drngnzr  19478  drngdomn  19519  qsssubdrg  20020  frlmphllem  20337  frlmphl  20338  cvsdivcl  23153  qcvs  23167  cphsubrglem  23197  rrxcph  23402  drnguc1p  24154  ig1peu  24155  ig1pcl  24159  ig1pdvds  24160  ig1prsp  24161  ply1lpir  24162  padicabv  25543  ofldchr  30149  reofld  30175  rearchi  30177  xrge0slmod  30179  zrhunitpreima  30357  elzrhunit  30358  qqhval2lem  30360  qqh0  30363  qqh1  30364  qqhf  30365  qqhghm  30367  qqhrhm  30368  qqhnm  30369  qqhucn  30371  zrhre  30398  qqhre  30399  lindsdom  33722  lindsenlbs  33723  matunitlindflem1  33724  matunitlindflem2  33725  matunitlindf  33726  dvalveclem  36811  dvhlveclem  36894  hlhilsrnglem  37739  sdrgacs  38277  cntzsdrg  38278  drhmsubc  42653  drngcat  42654  drhmsubcALTV  42671  drngcatALTV  42672  aacllem  43123
  Copyright terms: Public domain W3C validator