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

Theorem crngmgp 16672
Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.)
Hypothesis
Ref Expression
rngmgp.g  |-  G  =  (mulGrp `  R )
Assertion
Ref Expression
crngmgp  |-  ( R  e.  CRing  ->  G  e. CMnd )

Proof of Theorem crngmgp
StepHypRef Expression
1 rngmgp.g . . 3  |-  G  =  (mulGrp `  R )
21iscrng 16671 . 2  |-  ( R  e.  CRing 
<->  ( R  e.  Ring  /\  G  e. CMnd ) )
32simprbi 464 1  |-  ( R  e.  CRing  ->  G  e. CMnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   ` cfv 5437  CMndccmn 16296  mulGrpcmgp 16610   Ringcrg 16664   CRingccrg 16665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2740  df-rab 2743  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-br 4312  df-iota 5400  df-fv 5445  df-cring 16667
This theorem is referenced by:  crngcom  16678  gsummgp0  16718  prdscrngd  16724  crngbinom  16732  unitabl  16779  subrgcrng  16888  sraassa  17415  mplcoe2OLD  17569  mplbas2  17570  mplbas2OLD  17571  evlslem6  17617  evlslem6OLD  17618  evlslem3  17619  evlslem1  17620  ply1coeOLD  17766  evls1gsummul  17779  evl1gsummul  17813  mamuvs2  18329  matgsumcl  18364  madetsmelbas  18368  madetsmelbas2  18369  mdetleib2  18418  mdetf  18425  mdet1  18427  mdetrlin  18428  mdetrsca  18429  mdetralt  18433  mdetuni0  18446  smadiadetlem4  18494  amgmlem  22402  amgm  22403  wilthlem2  22426  wilthlem3  22427  lgseisenlem3  22709  lgseisenlem4  22710  mgpsumunsn  30782  mgpsumz  30783  mgpsumn  30784  mdetdiaglem  30958  mdetdiag  30959  mdetdiagid  30960
  Copyright terms: Public domain W3C validator