Theorem crngmgp 20239

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 20238	. 2 ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd))
3	2	simprbi 496	1 ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6560  CMndccmn 19799  mulGrpcmgp 20138  Ringcrg 20231  CRingccrg 20232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-cring 20234

This theorem is referenced by:  crngcom  20249  crngbascntr  20254  gsummgp0  20316  prdscrngd  20320  crngbinom  20333  unitabl  20385  subrgcrng  20576  frobrhm  21595  sraassaOLD  21891  mplbas2  22061  evlslem3  22105  evlslem6  22106  evlslem1  22107  evlsgsummul  22117  evls1gsummul  22330  evl1gsummul  22365  mamuvs2  22411  matgsumcl  22467  madetsmelbas  22471  madetsmelbas2  22472  mdetleib2  22595  mdetf  22602  mdetdiaglem  22605  mdetdiag  22606  mdetdiagid  22607  mdetrlin  22609  mdetrsca  22610  mdetralt  22615  mdetuni0  22628  smadiadetlem4  22676  chpscmat  22849  chp0mat  22853  chpidmat  22854  amgmlem  27034  amgm  27035  wilthlem2  27113  wilthlem3  27114  lgseisenlem3  27422  lgseisenlem4  27423  elrgspnsubrunlem1  33252  elrgspnsubrunlem2  33253  rlocaddval  33273  rlocmulval  33274  rloccring  33275  unitprodclb  33418  cringm4  33475  rprmdvdsprod  33563  1arithidomlem1  33564  1arithidom  33566  1arithufdlem3  33575  dfufd2lem  33578  mdetpmtr1  33823  aks6d1c1p2  42111  aks6d1c1p3  42112  aks6d1c1p4  42113  aks6d1c1p5  42114  aks6d1c1p7  42115  aks6d1c1p6  42116  aks6d1c1p8  42117  aks6d1c1  42118  evl1gprodd  42119  aks6d1c2lem3  42128  aks6d1c2lem4  42129  idomnnzgmulnz  42135  aks6d1c5lem0  42137  aks6d1c5lem3  42139  aks6d1c5lem2  42140  aks6d1c5  42141  deg1gprod  42142  aks6d1c6lem2  42173  aks6d1c6lem3  42174  aks6d1c6lem4  42175  aks6d1c6lem5  42179  aks5lem2  42189  aks5lem3a  42191  unitscyglem5  42201  pwsgprod  42559  evlsvvvallem  42576  selvvvval  42600  evlselv  42602  mhphf  42612  mgpsumunsn  48282  mgpsumz  48283  mgpsumn  48284  amgmwlem  49376  amgmlemALT  49377