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

Theorem ringgrp 19224
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 2825 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2825 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
3 eqid 2825 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2825 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19223 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp1bi 1139 1 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  wral 3142  cfv 6351  (class class class)co 7151  Basecbs 16475  +gcplusg 16557  .rcmulr 16558  Mndcmnd 17902  Grpcgrp 18035  mulGrpcmgp 19161  Ringcrg 19219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-nul 5206
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154  df-ring 19221
This theorem is referenced by:  ringmnd  19228  ring0cl  19241  ringacl  19250  ringcom  19251  ringabl  19252  ringlz  19259  ringrz  19260  ringnegl  19266  rngnegr  19267  ringmneg1  19268  ringmneg2  19269  ringm2neg  19270  ringsubdi  19271  rngsubdir  19272  mulgass2  19273  ringlghm  19276  ringrghm  19277  prdsringd  19284  imasring  19291  opprring  19303  dvdsrneg  19326  dvdsr02  19328  unitnegcl  19353  irrednegb  19383  dfrhm2  19391  isrhmd  19403  idrhm  19405  pwsco1rhm  19412  pwsco2rhm  19413  kerf1hrmOLD  19420  drnggrp  19432  subrgsubg  19463  cntzsubr  19490  pwsdiagrhm  19491  subrgacs  19501  isabvd  19513  abvneg  19527  abvsubtri  19528  abvtrivd  19533  srng0  19553  idsrngd  19555  lmodfgrp  19565  lmod0vs  19589  lmodvsneg  19600  lmodsubvs  19612  lmodsubdi  19613  lmodsubdir  19614  rmodislmodlem  19623  rmodislmod  19624  lssvnegcl  19650  lmodvsinv  19730  sralmod  19881  issubrngd2  19883  lidlsubg  19909  2idlcpbl  19928  0ringnnzr  19963  asclghm  20033  psrlmod  20102  psrdi  20107  psrdir  20108  psrring  20112  mpllsslem  20136  mplsubrg  20141  mplcoe1  20166  mplind  20202  evlslem2  20212  evlslem1  20215  mhplss  20261  coe1z  20350  coe1subfv  20353  evl1subd  20423  evl1gsumd  20438  cnfld0  20487  cnfldneg  20489  cnfldsub  20491  cnsubglem  20512  zringgrp  20540  mulgrhm  20563  chrdvds  20593  chrcong  20594  zncyg  20613  cygznlem3  20634  zrhpsgnelbas  20656  ip2subdi  20706  matinvgcell  20962  mat0dim0  20994  mat1ghm  21010  dmatsubcl  21025  dmatsgrp  21026  scmataddcl  21043  scmatsubcl  21044  scmatsgrp  21046  scmatsgrp1  21049  scmatghm  21060  mdetralt  21135  mdetero  21137  mdetunilem6  21144  mdetunilem9  21147  mdetuni0  21148  m2detleiblem6  21153  cpmatinvcl  21243  cpmatsubgpmat  21246  mat2pmatghm  21256  pm2mpghm  21342  chmatcl  21354  chpmat0d  21360  chpmat1d  21362  chpdmatlem1  21364  chpdmatlem2  21365  chpscmat  21368  chpscmatgsumbin  21370  chpscmatgsummon  21371  chp0mat  21372  chpidmat  21373  chfacfisf  21380  chfacfscmulgsum  21386  chfacfpmmulgsum  21390  cayhamlem1  21392  cpmadugsumlemF  21402  cpmidgsum2  21405  trggrp  22697  tlmtgp  22721  abvmet  23102  nrgdsdi  23191  nrgdsdir  23192  tngnrg  23200  cnngp  23305  cnfldtgp  23394  cnncvsaddassdemo  23684  cphsubrglem  23698  mdegldg  24577  mdeg0  24581  mdegaddle  24585  deg1add  24614  deg1suble  24618  deg1sub  24619  deg1sublt  24621  ply1nzb  24633  ply1divmo  24646  ply1divex  24647  r1pcl  24668  r1pid  24670  dvdsq1p  24671  dvdsr1p  24672  ply1remlem  24673  ply1rem  24674  ig1peu  24682  reefgim  24955  lgsqrlem1  25838  lgsqrlem2  25839  lgsqrlem3  25840  lgsqrlem4  25841  abvcxp  26107  dvdschrmulg  30774  freshmansdream  30775  dvrdir  30777  rmfsupp2  30782  orngsqr  30793  ornglmulle  30794  orngrmulle  30795  ornglmullt  30796  orngrmullt  30797  orngmullt  30798  ofldchr  30803  suborng  30804  isarchiofld  30806  rhmopp  30808  reofld  30829  linds2eq  30857  qsidomlem1  30871  qsidomlem2  30872  fedgmullem1  30913  ccfldsrarelvec  30944  zrhchr  31105  matunitlindflem1  34757  lfl0  36070  lflsub  36072  lfl0f  36074  lfladdass  36078  lfladd0l  36079  lflnegcl  36080  lflnegl  36081  ldualvsubcl  36161  ldualvsubval  36162  lkrin  36169  erng0g  37999  lclkrlem2m  38524  lcfrlem2  38548  lcdvsubval  38623  mapdpglem30  38707  baerlem3lem1  38712  baerlem5alem1  38713  baerlem5blem1  38714  baerlem5blem2  38717  hdmapinvlem3  38925  hdmapinvlem4  38926  hdmapglem7b  38933  hbtlem5  39595  mendlmod  39660  idomrootle  39662  c0rhm  44017  c0rnghm  44018  zrrnghm  44022  lidldomn1  44026  invginvrid  44249  evl1at0  44279  linply1  44281
  Copyright terms: Public domain W3C validator