Theorem drngring 20653

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ∖ cdif 3895  {csn 4575  ‘cfv 6486  Basecbs 17122  0_gc0g 17345  Ringcrg 20153  Unitcui 20275  DivRingcdr 20646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-drng 20648

This theorem is referenced by:  drngringd  20654  drngid  20663  drngunz  20664  drngnzr  20665  drngdomn  20666  drngmcl  20667  drnginvrcl  20670  drnginvrn0  20671  drnginvrl  20673  drnginvrr  20674  drngmul0orOLD  20678  drhmsubc  20698  drngcat  20699  sdrgid  20709  sdrgacs  20718  cntzsdrg  20719  primefld  20722  rlmlvec  21140  drngnidl  21182  drnglpir  21271  qsssubdrg  21365  ofldchr  21515  frlmlvec  21700  frlmphllem  21719  mpllvec  21958  cvsdivcl  25061  qcvs  25075  cphsubrglem  25105  rrxcph  25320  rrx0  25325  drnguc1p  26107  ig1peu  26108  ig1pcl  26112  ig1pdvds  26113  ig1prsp  26114  ply1lpir  26115  padicabv  27569  reofld  33315  rearchi  33318  xrge0slmod  33320  drng0mxidl  33448  drngmxidl  33449  zringfrac  33526  sradrng  33615  drgext0gsca  33625  drgextlsp  33627  rlmdim  33643  rgmoddimOLD  33644  frlmdim  33645  matdim  33649  drngdimgt0  33652  fedgmullem1  33663  fedgmullem2  33664  fedgmul  33665  fldextid  33693  extdg1id  33700  ccfldsrarelvec  33705  zrhunitpreima  34010  elzrhunit  34011  qqhval2lem  34015  qqh0  34018  qqh1  34019  qqhf  34020  qqhghm  34022  qqhrhm  34023  qqhnm  34024  qqhucn  34026  zrhre  34053  qqhre  34054  lindsdom  37674  lindsenlbs  37675  matunitlindflem1  37676  matunitlindflem2  37677  matunitlindf  37678  dvalveclem  41144  dvhlveclem  41227  hlhilsrnglem  42072  fldhmf1  42203  ricdrng1  42646  0prjspnrel  42745  drhmsubcALTV  48453  drngcatALTV  48454  aacllem  49926