Theorem ringgrp 20210

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 2737	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2737	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2737	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2737	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20209	. 2 ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1146	1 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Mndcmnd 18693  Grpcgrp 18900  mulGrpcmgp 20112  Ringcrg 20205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-ring 20207

This theorem is referenced by:  ringgrpd  20214  ringmnd  20215  ring0cl  20239  ringacl  20250  ringabl  20253  ringnegl  20274  ringnegr  20275  ringmneg1  20276  ringmneg2  20277  mulgass2  20281  ringlghm  20284  ringrghm  20285  prdsringd  20291  imasring  20301  dvdsrneg  20341  dvdsr02  20343  unitnegcl  20368  dvrdir  20383  irrednegb  20402  dfrhm2  20445  isrhmd  20458  idrhm  20460  pwsco1rhm  20470  pwsco2rhm  20471  rhmopp  20477  0ringnnzr  20493  c0rhm  20502  c0rnghm  20503  zrrnghm  20504  subrgsubg  20545  cntzsubr  20574  pwsdiagrhm  20575  subrgacs  20768  isabvd  20780  abvneg  20794  abvsubtri  20795  abvtrivd  20800  srng0  20822  idsrngd  20824  orngsqr  20834  ornglmulle  20835  orngrmulle  20836  ornglmullt  20837  orngrmullt  20838  orngmullt  20839  suborng  20844  lmodfgrp  20855  lmod0vs  20881  lmodvsneg  20892  lmodsubvs  20904  lmodsubdi  20905  lmodsubdir  20906  rmodislmodlem  20915  rmodislmod  20916  lmodvsinv  21023  sralmod  21174  issubrgd  21176  lidlsubg  21213  cnfld0  21382  cnfldneg  21385  cnfldsub  21387  cnsubglem  21405  zringgrp  21442  mulgrhm  21467  chrdvds  21516  chrcong  21517  dvdschrmulg  21518  zncyg  21538  cygznlem3  21559  freshmansdream  21564  zrhpsgnelbas  21584  ip2subdi  21634  asclghm  21872  psrlmod  21948  psrring  21958  mpllsslem  21988  mplsubrg  21993  mplcoe1  22025  mplind  22058  evlslem2  22067  coe1z  22238  coe1subfv  22241  evl1subd  22317  evl1gsumd  22332  matinvgcell  22410  mat0dim0  22442  mat1ghm  22458  dmatsubcl  22473  dmatsgrp  22474  scmataddcl  22491  scmatsubcl  22492  scmatsgrp  22494  scmatsgrp1  22497  scmatghm  22508  mdetralt  22583  mdetero  22585  mdetunilem6  22592  mdetunilem9  22595  mdetuni0  22596  m2detleiblem6  22601  cpmatinvcl  22692  cpmatsubgpmat  22695  mat2pmatghm  22705  pm2mpghm  22791  chmatcl  22803  chpmat0d  22809  chpmat1d  22811  chpdmatlem1  22813  chpdmatlem2  22814  chpscmat  22817  chpscmatgsumbin  22819  chpscmatgsummon  22820  chp0mat  22821  chpidmat  22822  chfacfisf  22829  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  cayhamlem1  22841  cpmadugsumlemF  22851  cpmidgsum2  22854  trggrp  24147  tlmtgp  24171  abvmet  24550  nrgdsdi  24640  nrgdsdir  24641  tngnrg  24649  cnngp  24754  cnfldtgp  24846  cnncvsaddassdemo  25140  cphsubrglem  25154  mdegldg  26041  mdeg0  26045  mdegaddle  26049  deg1add  26078  deg1suble  26082  deg1sub  26083  deg1sublt  26085  ply1nzb  26098  ply1divmo  26111  ply1divex  26112  r1pcl  26134  r1pid  26136  dvdsq1p  26138  dvdsr1p  26139  ply1remlem  26140  ply1rem  26141  idomrootle  26148  ig1peu  26150  reefgim  26428  lgsqrlem1  27323  lgsqrlem2  27324  lgsqrlem3  27325  lgsqrlem4  27326  abvcxp  27592  isarchiofld  33275  rmfsupp2  33314  reofld  33418  linds2eq  33456  qsidomlem1  33527  qsidomlem2  33528  qsnzr  33530  mxidlprm  33545  zringfrac  33629  esplyind  33734  vietadeg1  33737  fedgmullem1  33789  ccfldsrarelvec  33831  zrhchr  34134  matunitlindflem1  37951  lfl0  39525  lflsub  39527  lfl0f  39529  lfladdass  39533  lfladd0l  39534  lflnegcl  39535  lflnegl  39536  ldualvsubcl  39616  ldualvsubval  39617  lkrin  39624  erng0g  41454  lclkrlem2m  41979  lcfrlem2  42003  lcdvsubval  42078  mapdpglem30  42162  baerlem3lem1  42167  baerlem5alem1  42168  baerlem5blem1  42169  baerlem5blem2  42172  hdmapinvlem3  42380  hdmapinvlem4  42381  hdmapglem7b  42388  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6isolem2  42628  aks5lem3a  42642  aks5lem7  42653  hbtlem5  43574  mendlmod  43635  lidldomn1  48719  invginvrid  48855  evl1at0  48879  linply1  48881