Theorem crngmgp 20150

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

Step	Hyp	Ref	Expression
1		ringmgp.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
2	1	iscrng 20149	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd))
3	2	simprbi 496	1 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  CMndccmn 19710  mulGrpcmgp 20049  Ringcrg 20142  CRingccrg 20143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-cring 20145

This theorem is referenced by:  crngcom  20160  crngbascntr  20165  gsummgp0  20227  prdscrngd  20231  crngbinom  20244  unitabl  20293  subrgcrng  20484  frobrhm  21485  sraassaOLD  21779  mplbas2  21949  evlslem3  21987  evlslem6  21988  evlslem1  21989  evlsgsummul  21999  evls1gsummul  22212  evl1gsummul  22247  mamuvs2  22293  matgsumcl  22347  madetsmelbas  22351  madetsmelbas2  22352  mdetleib2  22475  mdetf  22482  mdetdiaglem  22485  mdetdiag  22486  mdetdiagid  22487  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  mdetuni0  22508  smadiadetlem4  22556  chpscmat  22729  chp0mat  22733  chpidmat  22734  amgmlem  26900  amgm  26901  wilthlem2  26979  wilthlem3  26980  lgseisenlem3  27288  lgseisenlem4  27289  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  rlocaddval  33219  rlocmulval  33220  rloccring  33221  unitprodclb  33360  cringm4  33417  rprmdvdsprod  33505  1arithidomlem1  33506  1arithidom  33508  1arithufdlem3  33517  dfufd2lem  33520  mdetpmtr1  33813  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c1  42104  evl1gprodd  42105  aks6d1c2lem3  42114  aks6d1c2lem4  42115  idomnnzgmulnz  42121  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  deg1gprod  42128  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6lem5  42165  aks5lem2  42175  aks5lem3a  42177  unitscyglem5  42187  pwsgprod  42532  evlsvvvallem  42549  selvvvval  42573  evlselv  42575  mhphf  42585  mgpsumunsn  48349  mgpsumz  48350  mgpsumn  48351  amgmwlem  49791  amgmlemALT  49792