Theorem ringgrp 20157

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 2731	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2731	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2731	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2731	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20156	. 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 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  +_gcplusg 17161  ._rcmulr 17162  Mndcmnd 18642  Grpcgrp 18846  mulGrpcmgp 20059  Ringcrg 20152

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 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-ring 20154

This theorem is referenced by:  ringgrpd  20161  ringmnd  20162  ring0cl  20186  ringacl  20197  ringabl  20200  ringnegl  20221  ringnegr  20222  ringmneg1  20223  ringmneg2  20224  mulgass2  20228  ringlghm  20231  ringrghm  20232  prdsringd  20240  imasring  20249  dvdsrneg  20289  dvdsr02  20291  unitnegcl  20316  dvrdir  20331  irrednegb  20350  dfrhm2  20393  isrhmd  20406  idrhm  20408  pwsco1rhm  20418  pwsco2rhm  20419  rhmopp  20425  0ringnnzr  20441  c0rhm  20450  c0rnghm  20451  zrrnghm  20452  subrgsubg  20493  cntzsubr  20522  pwsdiagrhm  20523  subrgacs  20716  isabvd  20728  abvneg  20742  abvsubtri  20743  abvtrivd  20748  srng0  20770  idsrngd  20772  orngsqr  20782  ornglmulle  20783  orngrmulle  20784  ornglmullt  20785  orngrmullt  20786  orngmullt  20787  suborng  20792  lmodfgrp  20803  lmod0vs  20829  lmodvsneg  20840  lmodsubvs  20852  lmodsubdi  20853  lmodsubdir  20854  rmodislmodlem  20863  rmodislmod  20864  lmodvsinv  20971  sralmod  21122  issubrgd  21124  lidlsubg  21161  cnfld0  21330  cnfldneg  21333  cnfldsub  21335  cnsubglem  21353  zringgrp  21390  mulgrhm  21415  chrdvds  21464  chrcong  21465  dvdschrmulg  21466  zncyg  21486  cygznlem3  21507  freshmansdream  21512  zrhpsgnelbas  21532  ip2subdi  21582  asclghm  21821  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  33166  rmfsupp2  33203  reofld  33306  linds2eq  33344  qsidomlem1  33415  qsidomlem2  33416  qsnzr  33418  mxidlprm  33433  zringfrac  33517  fedgmullem1  33640  ccfldsrarelvec  33682  zrhchr  33985  matunitlindflem1  37662  lfl0  39110  lflsub  39112  lfl0f  39114  lfladdass  39118  lfladd0l  39119  lflnegcl  39120  lflnegl  39121  ldualvsubcl  39201  ldualvsubval  39202  lkrin  39209  erng0g  41039  lclkrlem2m  41564  lcfrlem2  41588  lcdvsubval  41663  mapdpglem30  41747  baerlem3lem1  41752  baerlem5alem1  41753  baerlem5blem1  41754  baerlem5blem2  41757  hdmapinvlem3  41965  hdmapinvlem4  41966  hdmapglem7b  41973  aks6d1c6lem2  42210  aks6d1c6lem3  42211  aks6d1c6isolem2  42214  aks5lem3a  42228  aks5lem7  42239  hbtlem5  43167  mendlmod  43228  lidldomn1  48268  invginvrid  48404  evl1at0  48429  linply1  48431