Theorem drngring 20736

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ∖ cdif 3948  {csn 4626  ‘cfv 6561  Basecbs 17247  0_gc0g 17484  Ringcrg 20230  Unitcui 20355  DivRingcdr 20729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-drng 20731

This theorem is referenced by:  drngringd  20737  drngid  20746  drngunz  20747  drngnzr  20748  drngdomn  20749  drngmcl  20750  drnginvrcl  20753  drnginvrn0  20754  drnginvrl  20756  drnginvrr  20757  drngmul0orOLD  20761  drhmsubc  20782  drngcat  20783  sdrgid  20793  sdrgacs  20802  cntzsdrg  20803  primefld  20806  rlmlvec  21211  drngnidl  21253  drnglpir  21342  qsssubdrg  21444  frlmlvec  21781  frlmphllem  21800  mpllvec  22040  cvsdivcl  25166  qcvs  25181  cphsubrglem  25211  rrxcph  25426  rrx0  25431  drnguc1p  26213  ig1peu  26214  ig1pcl  26218  ig1pdvds  26219  ig1prsp  26220  ply1lpir  26221  padicabv  27674  ofldchr  33344  reofld  33372  rearchi  33374  xrge0slmod  33376  drng0mxidl  33504  drngmxidl  33505  zringfrac  33582  sradrng  33633  drgext0gsca  33642  drgextlsp  33644  rlmdim  33660  rgmoddimOLD  33661  frlmdim  33662  matdim  33666  drngdimgt0  33669  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  fldextid  33710  extdg1id  33716  ccfldsrarelvec  33721  zrhunitpreima  33977  elzrhunit  33978  qqhval2lem  33982  qqh0  33985  qqh1  33986  qqhf  33987  qqhghm  33989  qqhrhm  33990  qqhnm  33991  qqhucn  33993  zrhre  34020  qqhre  34021  lindsdom  37621  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  dvalveclem  41027  dvhlveclem  41110  hlhilsrnglem  41959  fldhmf1  42091  ricdrng1  42538  0prjspnrel  42637  drhmsubcALTV  48245  drngcatALTV  48246  aacllem  49320