MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringgrp Structured version   Visualization version   GIF version

Theorem ringgrp 18324
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.
StepHypRef Expression
1 eqid 2610 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2610 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
3 eqid 2610 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2610 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 18323 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp1bi 1069 1 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  wral 2896  cfv 5790  (class class class)co 6527  Basecbs 15644  +gcplusg 15717  .rcmulr 15718  Mndcmnd 17066  Grpcgrp 17194  mulGrpcmgp 18261  Ringcrg 18319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4712
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-iota 5754  df-fv 5798  df-ov 6530  df-ring 18321
This theorem is referenced by:  ringmnd  18328  ring0cl  18341  ringacl  18350  ringcom  18351  ringabl  18352  ringlz  18359  ringrz  18360  ringnegl  18366  rngnegr  18367  ringmneg1  18368  ringmneg2  18369  ringm2neg  18370  ringsubdi  18371  rngsubdir  18372  mulgass2  18373  ringlghm  18376  ringrghm  18377  prdsringd  18384  imasring  18391  opprring  18403  dvdsrneg  18426  dvdsr02  18428  unitnegcl  18453  irrednegb  18483  dfrhm2  18489  isrhmd  18501  idrhm  18503  pwsco1rhm  18510  pwsco2rhm  18511  kerf1hrm  18515  drnggrp  18527  subrgsubg  18558  cntzsubr  18584  pwsdiagrhm  18585  isabvd  18592  abvneg  18606  abvsubtri  18607  abvtrivd  18612  srng0  18632  idsrngd  18634  lmodfgrp  18644  lmod0vs  18668  lmodvsneg  18679  lmodsubvs  18691  lmodsubdi  18692  lmodsubdir  18693  lssvnegcl  18726  lmodvsinv  18806  sralmod  18957  issubrngd2  18959  lidlsubg  18985  2idlcpbl  19004  0ringnnzr  19039  asclghm  19108  psrlmod  19171  psrdi  19176  psrdir  19177  psrring  19181  mpllsslem  19205  mplsubrg  19210  mplcoe1  19235  mplind  19272  evlslem2  19282  evlslem1  19285  coe1z  19403  coe1subfv  19406  evl1subd  19476  evl1gsumd  19491  cnfld0  19538  cnfldneg  19540  cnfldsub  19542  cnsubglem  19563  zringgrp  19591  mulgrhm  19613  chrdvds  19643  chrcong  19644  zncyg  19664  cygznlem3  19685  zrhpsgnelbas  19707  ip2subdi  19756  matinvgcell  20008  mat0dim0  20040  mat1ghm  20056  dmatsubcl  20071  dmatsgrp  20072  scmataddcl  20089  scmatsubcl  20090  scmatsgrp  20092  scmatsgrp1  20095  scmatghm  20106  mdetralt  20181  mdetero  20183  mdetunilem6  20190  mdetunilem9  20193  mdetuni0  20194  m2detleiblem6  20199  cpmatinvcl  20289  cpmatsubgpmat  20292  mat2pmatghm  20302  pm2mpghm  20388  chmatcl  20400  chpmat0d  20406  chpmat1d  20408  chpdmatlem1  20410  chpdmatlem2  20411  chpscmat  20414  chpscmatgsumbin  20416  chpscmatgsummon  20417  chp0mat  20418  chpidmat  20419  chfacfisf  20426  chfacfscmulgsum  20432  chfacfpmmulgsum  20436  cayhamlem1  20438  cpmadugsumlemF  20448  cpmidgsum2  20451  trggrp  21733  tlmtgp  21757  abvmet  22138  nrgdsdi  22227  nrgdsdir  22228  tngnrg  22236  cnngp  22341  cnfldtgp  22428  cnncvsaddassdemo  22716  cphsubrglem  22730  mdegldg  23575  mdeg0  23579  mdegaddle  23583  deg1add  23612  deg1suble  23616  deg1sub  23617  deg1sublt  23619  ply1nzb  23631  ply1divmo  23644  ply1divex  23645  r1pcl  23666  r1pid  23668  dvdsq1p  23669  dvdsr1p  23670  ply1remlem  23671  ply1rem  23672  ig1peu  23680  reefgim  23953  lgsqrlem1  24816  lgsqrlem2  24817  lgsqrlem3  24818  lgsqrlem4  24819  abvcxp  25049  dvrdir  28915  orngsqr  28929  ornglmulle  28930  orngrmulle  28931  ornglmullt  28932  orngrmullt  28933  orngmullt  28934  ofldchr  28939  suborng  28940  isarchiofld  28942  rhmopp  28944  reofld  28965  zrhchr  29142  matunitlindflem1  32369  lfl0  33164  lflsub  33166  lfl0f  33168  lfladdass  33172  lfladd0l  33173  lflnegcl  33174  lflnegl  33175  ldualvsubcl  33255  ldualvsubval  33256  lkrin  33263  erng0g  35094  lclkrlem2m  35620  lcfrlem2  35644  lcdvsubval  35719  mapdpglem30  35803  baerlem3lem1  35808  baerlem5alem1  35809  baerlem5blem1  35810  baerlem5blem2  35813  hdmapinvlem3  36024  hdmapinvlem4  36025  hdmapglem7b  36032  hbtlem5  36511  mendlmod  36576  subrgacs  36583  idomrootle  36586  c0rhm  41694  c0rnghm  41695  zrrnghm  41699  lidldomn1  41703  invginvrid  41934  evl1at0  41965  linply1  41967
  Copyright terms: Public domain W3C validator