Theorem drngring 20713

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∖ cdif 3886  {csn 4567  ‘cfv 6498  Basecbs 17179  0_gc0g 17402  Ringcrg 20214  Unitcui 20335  DivRingcdr 20706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-drng 20708

This theorem is referenced by:  drngringd  20714  drngid  20723  drngunz  20724  drngnzr  20725  drngdomn  20726  drngmcl  20727  drnginvrcl  20730  drnginvrn0  20731  drnginvrl  20733  drnginvrr  20734  drngmul0orOLD  20738  drhmsubc  20758  drngcat  20759  sdrgid  20769  sdrgacs  20778  cntzsdrg  20779  primefld  20782  rlmlvec  21199  drngnidl  21241  drnglpir  21330  qsssubdrg  21406  ofldchr  21556  frlmlvec  21741  frlmphllem  21760  mpllvec  21998  cvsdivcl  25100  qcvs  25114  cphsubrglem  25144  rrxcph  25359  rrx0  25364  drnguc1p  26139  ig1peu  26140  ig1pcl  26144  ig1pdvds  26145  ig1prsp  26146  ply1lpir  26147  padicabv  27593  reofld  33403  rearchi  33406  xrge0slmod  33408  drng0mxidl  33536  drngmxidl  33537  zringfrac  33614  sradrng  33726  drgext0gsca  33736  drgextlsp  33738  rlmdim  33754  frlmdim  33755  matdim  33759  drngdimgt0  33762  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  fldextid  33803  extdg1id  33810  ccfldsrarelvec  33815  zrhunitpreima  34120  elzrhunit  34121  qqhval2lem  34125  qqh0  34128  qqh1  34129  qqhf  34130  qqhghm  34132  qqhrhm  34133  qqhnm  34134  qqhucn  34136  zrhre  34163  qqhre  34164  lindsdom  37935  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  dvalveclem  41471  dvhlveclem  41554  hlhilsrnglem  42399  fldhmf1  42529  ricdrng1  42973  0prjspnrel  43060  drhmsubcALTV  48805  drngcatALTV  48806  aacllem  50276