Theorem drngring 20765

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ∖ cdif 3901  {csn 4581  ‘cfv 6517  Basecbs 17228  0_gc0g 17451  Ringcrg 20262  Unitcui 20383  DivRingcdr 20758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-drng 20760

This theorem is referenced by:  drngringd  20766  drngid  20775  drngunz  20776  drngnzr  20777  drngdomn  20778  drngmcl  20779  drnginvrcl  20782  drnginvrn0  20783  drnginvrl  20785  drnginvrr  20786  drngmul0orOLD  20790  drhmsubc  20810  drngcat  20811  sdrgid  20821  sdrgacs  20830  cntzsdrg  20831  primefld  20834  rlmlvec  21251  drngnidl  21293  drnglpir  21382  qsssubdrg  21458  ofldchr  21608  frlmlvec  21793  frlmphllem  21812  mpllvec  22051  cvsdivcl  25175  qcvs  25189  cphsubrglem  25219  rrxcph  25434  rrx0  25439  drnguc1p  26214  ig1peu  26215  ig1pcl  26219  ig1pdvds  26220  ig1prsp  26221  ply1lpir  26222  padicabv  27671  reofld  33490  rearchi  33493  xrge0slmod  33495  drng0mxidl  33625  drngmxidl  33626  zringfrac  33711  sradrng  33840  drgext0gsca  33850  drgextlsp  33852  rlmdim  33868  frlmdim  33869  matdim  33873  drngdimgt0  33876  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  fldextid  33917  extdg1id  33924  ccfldsrarelvec  33929  zrhunitpreima  34234  elzrhunit  34235  qqhval2lem  34239  qqh0  34242  qqh1  34243  qqhf  34244  qqhghm  34246  qqhrhm  34247  qqhnm  34248  qqhucn  34250  zrhre  34277  qqhre  34278  lindsdom  38077  lindsenlbs  38078  matunitlindflem1  38079  matunitlindflem2  38080  matunitlindf  38081  dvalveclem  41613  dvhlveclem  41696  hlhilsrnglem  42541  fldhmf1  42671  ricdrng1  43110  0prjspnrel  43173  drhmsubcALTV  48915  drngcatALTV  48916  aacllem  50386