Theorem ringgrp 20217

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Mndcmnd 18700  Grpcgrp 18907  mulGrpcmgp 20119  Ringcrg 20212

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

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-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  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-ov 7366  df-ring 20214

This theorem is referenced by:  ringgrpd  20221  ringmnd  20222  ring0cl  20246  ringacl  20257  ringabl  20260  ringnegl  20281  ringnegr  20282  ringmneg1  20283  ringmneg2  20284  mulgass2  20288  ringlghm  20291  ringrghm  20292  prdsringd  20298  imasring  20308  dvdsrneg  20348  dvdsr02  20350  unitnegcl  20375  dvrdir  20390  irrednegb  20409  dfrhm2  20452  isrhmd  20466  idrhm  20468  pwsco1rhm  20480  pwsco2rhm  20481  rhmopp  20488  0ringnnzr  20504  c0rhm  20513  c0rnghm  20514  zrrnghm  20515  subrgsubg  20556  cntzsubr  20585  pwsdiagrhm  20586  subrgacs  20779  isabvd  20791  abvneg  20805  abvsubtri  20806  abvtrivd  20811  srng0  20833  idsrngd  20835  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  ornglmullt  20848  orngrmullt  20849  orngmullt  20850  suborng  20855  lmodfgrp  20866  lmod0vs  20892  lmodvsneg  20903  lmodsubvs  20915  lmodsubdi  20916  lmodsubdir  20917  rmodislmodlem  20926  rmodislmod  20927  lmodvsinv  21033  sralmod  21184  issubrgd  21186  lidlsubg  21223  cnfld0  21378  cnfldneg  21380  cnfldsub  21382  cnsubglem  21398  zringgrp  21434  mulgrhm  21459  chrdvds  21508  chrcong  21509  dvdschrmulg  21510  zncyg  21530  cygznlem3  21551  freshmansdream  21556  zrhpsgnelbas  21576  ip2subdi  21626  asclghm  21864  psrlmod  21941  psrring  21951  mpllsslem  21981  mplsubrg  21986  mplcoe1  22020  mplind  22053  evlslem2  22062  coe1z  22256  coe1subfv  22259  evl1subd  22335  evl1gsumd  22350  matinvgcell  22425  mat0dim0  22457  mat1ghm  22473  dmatsubcl  22488  dmatsgrp  22489  scmataddcl  22506  scmatsubcl  22507  scmatsgrp  22509  scmatsgrp1  22512  scmatghm  22523  mdetralt  22598  mdetero  22600  mdetunilem6  22607  mdetunilem9  22610  mdetuni0  22611  m2detleiblem6  22616  cpmatinvcl  22707  cpmatsubgpmat  22710  mat2pmatghm  22720  pm2mpghm  22806  chmatcl  22818  chpmat0d  22824  chpmat1d  22826  chpdmatlem1  22828  chpdmatlem2  22829  chpscmat  22832  chpscmatgsumbin  22834  chpscmatgsummon  22835  chp0mat  22836  chpidmat  22837  chfacfisf  22844  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  cayhamlem1  22856  cpmadugsumlemF  22866  cpmidgsum2  22869  trggrp  24162  tlmtgp  24186  abvmet  24565  nrgdsdi  24655  nrgdsdir  24656  tngnrg  24664  cnngp  24769  cnfldtgp  24861  cnncvsaddassdemo  25155  cphsubrglem  25169  mdegldg  26056  mdeg0  26060  mdegaddle  26064  deg1add  26093  deg1suble  26097  deg1sub  26098  deg1sublt  26100  ply1nzb  26113  ply1divmo  26126  ply1divex  26127  r1pcl  26149  r1pid  26151  dvdsq1p  26153  dvdsr1p  26154  ply1remlem  26155  ply1rem  26156  idomrootle  26163  ig1peu  26165  reefgim  26440  lgsqrlem1  27334  lgsqrlem2  27335  lgsqrlem3  27336  lgsqrlem4  27337  abvcxp  27603  isarchiofld  33287  rmfsupp2  33326  reofld  33433  linds2eq  33471  qsidomlem1  33542  qsidomlem2  33543  qsnzr  33545  mxidlprm  33560  zringfrac  33644  esplyind  33766  vietadeg1  33769  fedgmullem1  33820  ccfldsrarelvec  33862  zrhchr  34165  matunitlindflem1  37990  lfl0  39564  lflsub  39566  lfl0f  39568  lfladdass  39572  lfladd0l  39573  lflnegcl  39574  lflnegl  39575  ldualvsubcl  39655  ldualvsubval  39656  lkrin  39663  erng0g  41493  lclkrlem2m  42018  lcfrlem2  42042  lcdvsubval  42117  mapdpglem30  42201  baerlem3lem1  42206  baerlem5alem1  42207  baerlem5blem1  42208  baerlem5blem2  42211  hdmapinvlem3  42419  hdmapinvlem4  42420  hdmapglem7b  42427  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c6isolem2  42667  aks5lem3a  42681  aks5lem7  42692  hbtlem5  43580  mendlmod  43641  lidldomn1  48729  invginvrid  48865  evl1at0  48889  linply1  48891