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

Theorem crngmgp 19302
 Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
Hypothesis
Ref Expression
ringmgp.g 𝐺 = (mulGrp‘𝑅)
Assertion
Ref Expression
crngmgp (𝑅 ∈ CRing → 𝐺 ∈ CMnd)

Proof of Theorem crngmgp
StepHypRef Expression
1 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
21iscrng 19301 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd))
32simprbi 500 1 (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2112  ‘cfv 6328  CMndccmn 18902  mulGrpcmgp 19236  Ringcrg 19294  CRingccrg 19295 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-cring 19297 This theorem is referenced by:  crngcom  19312  gsummgp0  19358  prdscrngd  19363  crngbinom  19371  unitabl  19418  subrgcrng  19536  sraassa  20560  mplbas2  20714  evlslem3  20756  evlslem6  20757  evlslem1  20758  evlsgsummul  20768  evls1gsummul  20953  evl1gsummul  20988  mamuvs2  21015  matgsumcl  21069  madetsmelbas  21073  madetsmelbas2  21074  mdetleib2  21197  mdetf  21204  mdetdiaglem  21207  mdetdiag  21208  mdetdiagid  21209  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  mdetuni0  21230  smadiadetlem4  21278  chpscmat  21451  chp0mat  21455  chpidmat  21456  amgmlem  25579  amgm  25580  wilthlem2  25658  wilthlem3  25659  lgseisenlem3  25965  lgseisenlem4  25966  frobrhm  30914  cringm4  31034  mdetpmtr1  31180  mgpsumunsn  44760  mgpsumz  44761  mgpsumn  44762  amgmwlem  45327  amgmlemALT  45328
 Copyright terms: Public domain W3C validator