Theorem drngring 20645

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∖ cdif 3911  {csn 4589  ‘cfv 6511  Basecbs 17179  0_gc0g 17402  Ringcrg 20142  Unitcui 20264  DivRingcdr 20638

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-drng 20640

This theorem is referenced by:  drngringd  20646  drngid  20655  drngunz  20656  drngnzr  20657  drngdomn  20658  drngmcl  20659  drnginvrcl  20662  drnginvrn0  20663  drnginvrl  20665  drnginvrr  20666  drngmul0orOLD  20670  drhmsubc  20690  drngcat  20691  sdrgid  20701  sdrgacs  20710  cntzsdrg  20711  primefld  20714  rlmlvec  21111  drngnidl  21153  drnglpir  21242  qsssubdrg  21343  frlmlvec  21670  frlmphllem  21689  mpllvec  21929  cvsdivcl  25033  qcvs  25047  cphsubrglem  25077  rrxcph  25292  rrx0  25297  drnguc1p  26079  ig1peu  26080  ig1pcl  26084  ig1pdvds  26085  ig1prsp  26086  ply1lpir  26087  padicabv  27541  ofldchr  33292  reofld  33315  rearchi  33317  xrge0slmod  33319  drng0mxidl  33447  drngmxidl  33448  zringfrac  33525  sradrng  33578  drgext0gsca  33587  drgextlsp  33589  rlmdim  33605  rgmoddimOLD  33606  frlmdim  33607  matdim  33611  drngdimgt0  33614  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  fldextid  33655  extdg1id  33661  ccfldsrarelvec  33666  zrhunitpreima  33966  elzrhunit  33967  qqhval2lem  33971  qqh0  33974  qqh1  33975  qqhf  33976  qqhghm  33978  qqhrhm  33979  qqhnm  33980  qqhucn  33982  zrhre  34009  qqhre  34010  lindsdom  37608  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  dvalveclem  41019  dvhlveclem  41102  hlhilsrnglem  41947  fldhmf1  42078  ricdrng1  42516  0prjspnrel  42615  drhmsubcALTV  48317  drngcatALTV  48318  aacllem  49790