Theorem drngring 20715

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∖ cdif 3887  {csn 4562  ‘cfv 6492  Basecbs 17177  0_gc0g 17400  Ringcrg 20212  Unitcui 20333  DivRingcdr 20708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-drng 20710

This theorem is referenced by:  drngringd  20716  drngid  20725  drngunz  20726  drngnzr  20727  drngdomn  20728  drngmcl  20729  drnginvrcl  20732  drnginvrn0  20733  drnginvrl  20735  drnginvrr  20736  drngmul0orOLD  20740  drhmsubc  20760  drngcat  20761  sdrgid  20771  sdrgacs  20780  cntzsdrg  20781  primefld  20784  rlmlvec  21201  drngnidl  21243  drnglpir  21332  qsssubdrg  21408  ofldchr  21558  frlmlvec  21743  frlmphllem  21762  mpllvec  22001  cvsdivcl  25125  qcvs  25139  cphsubrglem  25169  rrxcph  25384  rrx0  25389  drnguc1p  26164  ig1peu  26165  ig1pcl  26169  ig1pdvds  26170  ig1prsp  26171  ply1lpir  26172  padicabv  27618  reofld  33433  rearchi  33436  xrge0slmod  33438  drng0mxidl  33566  drngmxidl  33567  zringfrac  33644  sradrng  33773  drgext0gsca  33783  drgextlsp  33785  rlmdim  33801  frlmdim  33802  matdim  33806  drngdimgt0  33809  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  fldextid  33850  extdg1id  33857  ccfldsrarelvec  33862  zrhunitpreima  34167  elzrhunit  34168  qqhval2lem  34172  qqh0  34175  qqh1  34176  qqhf  34177  qqhghm  34179  qqhrhm  34180  qqhnm  34181  qqhucn  34183  zrhre  34210  qqhre  34211  lindsdom  37988  lindsenlbs  37989  matunitlindflem1  37990  matunitlindflem2  37991  matunitlindf  37992  dvalveclem  41524  dvhlveclem  41607  hlhilsrnglem  42452  fldhmf1  42582  ricdrng1  43021  0prjspnrel  43084  drhmsubcALTV  48827  drngcatALTV  48828  aacllem  50298