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

Theorem ringgrp 19233
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 2821 . . 3 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2821 . . 3 (mulGrp‘𝑅) = (mulGrp‘𝑅)
3 eqid 2821 . . 3 (+g𝑅) = (+g𝑅)
4 eqid 2821 . . 3 (.r𝑅) = (.r𝑅)
51, 2, 3, 4isring 19232 . 2 (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ (mulGrp‘𝑅) ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r𝑅)(𝑦(+g𝑅)𝑧)) = ((𝑥(.r𝑅)𝑦)(+g𝑅)(𝑥(.r𝑅)𝑧)) ∧ ((𝑥(+g𝑅)𝑦)(.r𝑅)𝑧) = ((𝑥(.r𝑅)𝑧)(+g𝑅)(𝑦(.r𝑅)𝑧)))))
65simp1bi 1137 1 (𝑅 ∈ Ring → 𝑅 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wral 3138  cfv 6349  (class class class)co 7145  Basecbs 16473  +gcplusg 16555  .rcmulr 16556  Mndcmnd 17901  Grpcgrp 18043  mulGrpcmgp 19170  Ringcrg 19228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-nul 5202
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-ring 19230
This theorem is referenced by:  ringmnd  19237  ring0cl  19250  ringacl  19259  ringcom  19260  ringabl  19261  ringlz  19268  ringrz  19269  ringnegl  19275  rngnegr  19276  ringmneg1  19277  ringmneg2  19278  ringm2neg  19279  ringsubdi  19280  rngsubdir  19281  mulgass2  19282  ringlghm  19285  ringrghm  19286  prdsringd  19293  imasring  19300  opprring  19312  dvdsrneg  19335  dvdsr02  19337  unitnegcl  19362  irrednegb  19392  dfrhm2  19400  isrhmd  19412  idrhm  19414  pwsco1rhm  19421  pwsco2rhm  19422  kerf1hrmOLD  19429  drnggrp  19441  subrgsubg  19472  cntzsubr  19499  pwsdiagrhm  19500  subrgacs  19510  isabvd  19522  abvneg  19536  abvsubtri  19537  abvtrivd  19542  srng0  19562  idsrngd  19564  lmodfgrp  19574  lmod0vs  19598  lmodvsneg  19609  lmodsubvs  19621  lmodsubdi  19622  lmodsubdir  19623  rmodislmodlem  19632  rmodislmod  19633  lssvnegcl  19659  lmodvsinv  19739  sralmod  19890  issubrngd2  19892  lidlsubg  19918  2idlcpbl  19937  0ringnnzr  19972  asclghm  20042  psrlmod  20111  psrdi  20116  psrdir  20117  psrring  20121  mpllsslem  20145  mplsubrg  20150  mplcoe1  20176  mplind  20212  evlslem2  20222  evlslem1  20225  mhplss  20272  coe1z  20361  coe1subfv  20364  evl1subd  20435  evl1gsumd  20450  cnfld0  20499  cnfldneg  20501  cnfldsub  20503  cnsubglem  20524  zringgrp  20552  mulgrhm  20575  chrdvds  20605  chrcong  20606  zncyg  20625  cygznlem3  20646  zrhpsgnelbas  20668  ip2subdi  20718  matinvgcell  20974  mat0dim0  21006  mat1ghm  21022  dmatsubcl  21037  dmatsgrp  21038  scmataddcl  21055  scmatsubcl  21056  scmatsgrp  21058  scmatsgrp1  21061  scmatghm  21072  mdetralt  21147  mdetero  21149  mdetunilem6  21156  mdetunilem9  21159  mdetuni0  21160  m2detleiblem6  21165  cpmatinvcl  21255  cpmatsubgpmat  21258  mat2pmatghm  21268  pm2mpghm  21354  chmatcl  21366  chpmat0d  21372  chpmat1d  21374  chpdmatlem1  21376  chpdmatlem2  21377  chpscmat  21380  chpscmatgsumbin  21382  chpscmatgsummon  21383  chp0mat  21384  chpidmat  21385  chfacfisf  21392  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  cayhamlem1  21404  cpmadugsumlemF  21414  cpmidgsum2  21417  trggrp  22709  tlmtgp  22733  abvmet  23114  nrgdsdi  23203  nrgdsdir  23204  tngnrg  23212  cnngp  23317  cnfldtgp  23406  cnncvsaddassdemo  23696  cphsubrglem  23710  mdegldg  24589  mdeg0  24593  mdegaddle  24597  deg1add  24626  deg1suble  24630  deg1sub  24631  deg1sublt  24633  ply1nzb  24645  ply1divmo  24658  ply1divex  24659  r1pcl  24680  r1pid  24682  dvdsq1p  24683  dvdsr1p  24684  ply1remlem  24685  ply1rem  24686  ig1peu  24694  reefgim  24967  lgsqrlem1  25850  lgsqrlem2  25851  lgsqrlem3  25852  lgsqrlem4  25853  abvcxp  26119  dvdschrmulg  30786  freshmansdream  30787  dvrdir  30789  rmfsupp2  30794  orngsqr  30805  ornglmulle  30806  orngrmulle  30807  ornglmullt  30808  orngrmullt  30809  orngmullt  30810  ofldchr  30815  suborng  30816  isarchiofld  30818  rhmopp  30820  reofld  30841  linds2eq  30869  qsidomlem1  30883  qsidomlem2  30884  fedgmullem1  30925  ccfldsrarelvec  30956  zrhchr  31117  matunitlindflem1  34770  lfl0  36083  lflsub  36085  lfl0f  36087  lfladdass  36091  lfladd0l  36092  lflnegcl  36093  lflnegl  36094  ldualvsubcl  36174  ldualvsubval  36175  lkrin  36182  erng0g  38012  lclkrlem2m  38537  lcfrlem2  38561  lcdvsubval  38636  mapdpglem30  38720  baerlem3lem1  38725  baerlem5alem1  38726  baerlem5blem1  38727  baerlem5blem2  38730  hdmapinvlem3  38938  hdmapinvlem4  38939  hdmapglem7b  38946  hbtlem5  39608  mendlmod  39673  idomrootle  39675  c0rhm  44081  c0rnghm  44082  zrrnghm  44086  lidldomn1  44090  invginvrid  44313  evl1at0  44343  linply1  44345
  Copyright terms: Public domain W3C validator