Theorem crngmgp 20176

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  CMndccmn 19709  mulGrpcmgp 20075  Ringcrg 20168  CRingccrg 20169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-cring 20171

This theorem is referenced by:  crngcom  20186  crngbascntr  20191  gsummgp0  20253  prdscrngd  20257  pwsgprod  20265  crngbinom  20271  unitabl  20320  subrgcrng  20508  frobrhm  21530  sraassaOLD  21825  mplbas2  21997  evlslem3  22035  evlslem6  22036  evlslem1  22037  evlsvvvallem  22046  evlsgsummul  22052  evls1gsummul  22269  evl1gsummul  22304  mamuvs2  22350  matgsumcl  22404  madetsmelbas  22408  madetsmelbas2  22409  mdetleib2  22532  mdetf  22539  mdetdiaglem  22542  mdetdiag  22543  mdetdiagid  22544  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetuni0  22565  smadiadetlem4  22613  chpscmat  22786  chp0mat  22790  chpidmat  22791  amgmlem  26956  amgm  26957  wilthlem2  27035  wilthlem3  27036  lgseisenlem3  27344  lgseisenlem4  27345  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  rlocaddval  33350  rlocmulval  33351  rloccring  33352  domnprodeq0  33358  unitprodclb  33470  cringm4  33527  rprmdvdsprod  33615  1arithidomlem1  33616  1arithidom  33618  1arithufdlem3  33627  dfufd2lem  33630  deg1prod  33664  evlextv  33707  vietalem  33735  mdetpmtr1  33980  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1p8  42369  aks6d1c1  42370  evl1gprodd  42371  aks6d1c2lem3  42380  aks6d1c2lem4  42381  idomnnzgmulnz  42387  aks6d1c5lem0  42389  aks6d1c5lem3  42391  aks6d1c5lem2  42392  aks6d1c5  42393  deg1gprod  42394  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6lem5  42431  aks5lem2  42441  aks5lem3a  42443  unitscyglem5  42453  selvvvval  42828  evlselv  42830  mhphf  42840  mgpsumunsn  48607  mgpsumz  48608  mgpsumn  48609  amgmwlem  50047  amgmlemALT  50048