Theorem ringgrp 20219

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 2736	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2736	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2736	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2736	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isring 20218	. 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 3051  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Mndcmnd 18702  Grpcgrp 18909  mulGrpcmgp 20121  Ringcrg 20214

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ring 20216

This theorem is referenced by:  ringgrpd  20223  ringmnd  20224  ring0cl  20248  ringacl  20259  ringabl  20262  ringnegl  20283  ringnegr  20284  ringmneg1  20285  ringmneg2  20286  mulgass2  20290  ringlghm  20293  ringrghm  20294  prdsringd  20300  imasring  20310  dvdsrneg  20350  dvdsr02  20352  unitnegcl  20377  dvrdir  20392  irrednegb  20411  dfrhm2  20454  isrhmd  20467  idrhm  20469  pwsco1rhm  20479  pwsco2rhm  20480  rhmopp  20486  0ringnnzr  20502  c0rhm  20511  c0rnghm  20512  zrrnghm  20513  subrgsubg  20554  cntzsubr  20583  pwsdiagrhm  20584  subrgacs  20777  isabvd  20789  abvneg  20803  abvsubtri  20804  abvtrivd  20809  srng0  20831  idsrngd  20833  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  ornglmullt  20846  orngrmullt  20847  orngmullt  20848  suborng  20853  lmodfgrp  20864  lmod0vs  20890  lmodvsneg  20901  lmodsubvs  20913  lmodsubdi  20914  lmodsubdir  20915  rmodislmodlem  20924  rmodislmod  20925  lmodvsinv  21031  sralmod  21182  issubrgd  21184  lidlsubg  21221  cnfld0  21376  cnfldneg  21378  cnfldsub  21380  cnsubglem  21396  zringgrp  21432  mulgrhm  21457  chrdvds  21506  chrcong  21507  dvdschrmulg  21508  zncyg  21528  cygznlem3  21549  freshmansdream  21554  zrhpsgnelbas  21574  ip2subdi  21624  asclghm  21862  psrlmod  21938  psrring  21948  mpllsslem  21978  mplsubrg  21983  mplcoe1  22015  mplind  22048  evlslem2  22057  coe1z  22228  coe1subfv  22231  evl1subd  22307  evl1gsumd  22322  matinvgcell  22400  mat0dim0  22432  mat1ghm  22448  dmatsubcl  22463  dmatsgrp  22464  scmataddcl  22481  scmatsubcl  22482  scmatsgrp  22484  scmatsgrp1  22487  scmatghm  22498  mdetralt  22573  mdetero  22575  mdetunilem6  22582  mdetunilem9  22585  mdetuni0  22586  m2detleiblem6  22591  cpmatinvcl  22682  cpmatsubgpmat  22685  mat2pmatghm  22695  pm2mpghm  22781  chmatcl  22793  chpmat0d  22799  chpmat1d  22801  chpdmatlem1  22803  chpdmatlem2  22804  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chp0mat  22811  chpidmat  22812  chfacfisf  22819  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cayhamlem1  22831  cpmadugsumlemF  22841  cpmidgsum2  22844  trggrp  24137  tlmtgp  24161  abvmet  24540  nrgdsdi  24630  nrgdsdir  24631  tngnrg  24639  cnngp  24744  cnfldtgp  24836  cnncvsaddassdemo  25130  cphsubrglem  25144  mdegldg  26031  mdeg0  26035  mdegaddle  26039  deg1add  26068  deg1suble  26072  deg1sub  26073  deg1sublt  26075  ply1nzb  26088  ply1divmo  26101  ply1divex  26102  r1pcl  26124  r1pid  26126  dvdsq1p  26128  dvdsr1p  26129  ply1remlem  26130  ply1rem  26131  idomrootle  26138  ig1peu  26140  reefgim  26415  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  abvcxp  27578  isarchiofld  33260  rmfsupp2  33299  reofld  33403  linds2eq  33441  qsidomlem1  33512  qsidomlem2  33513  qsnzr  33515  mxidlprm  33530  zringfrac  33614  esplyind  33719  vietadeg1  33722  fedgmullem1  33773  ccfldsrarelvec  33815  zrhchr  34118  matunitlindflem1  37937  lfl0  39511  lflsub  39513  lfl0f  39515  lfladdass  39519  lfladd0l  39520  lflnegcl  39521  lflnegl  39522  ldualvsubcl  39602  ldualvsubval  39603  lkrin  39610  erng0g  41440  lclkrlem2m  41965  lcfrlem2  41989  lcdvsubval  42064  mapdpglem30  42148  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem5blem2  42158  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem7b  42374  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6isolem2  42614  aks5lem3a  42628  aks5lem7  42639  hbtlem5  43556  mendlmod  43617  lidldomn1  48707  invginvrid  48843  evl1at0  48867  linply1  48869