Theorem ringgrp 20158

Description: A ring is a group. (Contributed by NM, 15-Sep-2011.)

Assertion

Ref	Expression
ringgrp	⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Proof of Theorem ringgrp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2733	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2733	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2733	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20157	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1145	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  +_gcplusg 17163  ._rcmulr 17164  Mndcmnd 18644  Grpcgrp 18848  mulGrpcmgp 20060  Ringcrg 20153

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  ax-nul 5246

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-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  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-ov 7355  df-ring 20155

This theorem is referenced by:  ringgrpd  20162  ringmnd  20163  ring0cl  20187  ringacl  20198  ringabl  20201  ringnegl  20222  ringnegr  20223  ringmneg1  20224  ringmneg2  20225  mulgass2  20229  ringlghm  20232  ringrghm  20233  prdsringd  20241  imasring  20250  dvdsrneg  20290  dvdsr02  20292  unitnegcl  20317  dvrdir  20332  irrednegb  20351  dfrhm2  20394  isrhmd  20407  idrhm  20409  pwsco1rhm  20419  pwsco2rhm  20420  rhmopp  20426  0ringnnzr  20442  c0rhm  20451  c0rnghm  20452  zrrnghm  20453  subrgsubg  20494  cntzsubr  20523  pwsdiagrhm  20524  subrgacs  20717  isabvd  20729  abvneg  20743  abvsubtri  20744  abvtrivd  20749  srng0  20771  idsrngd  20773  orngsqr  20783  ornglmulle  20784  orngrmulle  20785  ornglmullt  20786  orngrmullt  20787  orngmullt  20788  suborng  20793  lmodfgrp  20804  lmod0vs  20830  lmodvsneg  20841  lmodsubvs  20853  lmodsubdi  20854  lmodsubdir  20855  rmodislmodlem  20864  rmodislmod  20865  lmodvsinv  20972  sralmod  21123  issubrgd  21125  lidlsubg  21162  cnfld0  21331  cnfldneg  21334  cnfldsub  21336  cnsubglem  21354  zringgrp  21391  mulgrhm  21416  chrdvds  21465  chrcong  21466  dvdschrmulg  21467  zncyg  21487  cygznlem3  21508  freshmansdream  21513  zrhpsgnelbas  21533  ip2subdi  21583  asclghm  21822  psrlmod  21898  psrring  21908  mpllsslem  21938  mplsubrg  21943  mplcoe1  21973  mplind  22006  evlslem2  22015  coe1z  22178  coe1subfv  22181  evl1subd  22258  evl1gsumd  22273  matinvgcell  22351  mat0dim0  22383  mat1ghm  22399  dmatsubcl  22414  dmatsgrp  22415  scmataddcl  22432  scmatsubcl  22433  scmatsgrp  22435  scmatsgrp1  22438  scmatghm  22449  mdetralt  22524  mdetero  22526  mdetunilem6  22533  mdetunilem9  22536  mdetuni0  22537  m2detleiblem6  22542  cpmatinvcl  22633  cpmatsubgpmat  22636  mat2pmatghm  22646  pm2mpghm  22732  chmatcl  22744  chpmat0d  22750  chpmat1d  22752  chpdmatlem1  22754  chpdmatlem2  22755  chpscmat  22758  chpscmatgsumbin  22760  chpscmatgsummon  22761  chp0mat  22762  chpidmat  22763  chfacfisf  22770  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  cayhamlem1  22782  cpmadugsumlemF  22792  cpmidgsum2  22795  trggrp  24088  tlmtgp  24112  abvmet  24491  nrgdsdi  24581  nrgdsdir  24582  tngnrg  24590  cnngp  24695  cnfldtgp  24788  cnncvsaddassdemo  25091  cphsubrglem  25105  mdegldg  25999  mdeg0  26003  mdegaddle  26007  deg1add  26036  deg1suble  26040  deg1sub  26041  deg1sublt  26043  ply1nzb  26056  ply1divmo  26069  ply1divex  26070  r1pcl  26092  r1pid  26094  dvdsq1p  26096  dvdsr1p  26097  ply1remlem  26098  ply1rem  26099  idomrootle  26106  ig1peu  26108  reefgim  26388  lgsqrlem1  27285  lgsqrlem2  27286  lgsqrlem3  27287  lgsqrlem4  27288  abvcxp  27554  isarchiofld  33175  rmfsupp2  33212  reofld  33315  linds2eq  33353  qsidomlem1  33424  qsidomlem2  33425  qsnzr  33427  mxidlprm  33442  zringfrac  33526  esplyind  33613  fedgmullem1  33663  ccfldsrarelvec  33705  zrhchr  34008  matunitlindflem1  37677  lfl0  39185  lflsub  39187  lfl0f  39189  lfladdass  39193  lfladd0l  39194  lflnegcl  39195  lflnegl  39196  ldualvsubcl  39276  ldualvsubval  39277  lkrin  39284  erng0g  41114  lclkrlem2m  41639  lcfrlem2  41663  lcdvsubval  41738  mapdpglem30  41822  baerlem3lem1  41827  baerlem5alem1  41828  baerlem5blem1  41829  baerlem5blem2  41832  hdmapinvlem3  42040  hdmapinvlem4  42041  hdmapglem7b  42048  aks6d1c6lem2  42285  aks6d1c6lem3  42286  aks6d1c6isolem2  42289  aks5lem3a  42303  aks5lem7  42314  hbtlem5  43246  mendlmod  43307  lidldomn1  48356  invginvrid  48492  evl1at0  48517  linply1  48519