Theorem crngmgp 20154

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ‘cfv 6476  CMndccmn 19687  mulGrpcmgp 20053  Ringcrg 20146  CRingccrg 20147

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-cring 20149

This theorem is referenced by:  crngcom  20164  crngbascntr  20169  gsummgp0  20231  prdscrngd  20235  crngbinom  20248  unitabl  20297  subrgcrng  20485  frobrhm  21507  sraassaOLD  21802  mplbas2  21972  evlslem3  22010  evlslem6  22011  evlslem1  22012  evlsgsummul  22022  evls1gsummul  22235  evl1gsummul  22270  mamuvs2  22316  matgsumcl  22370  madetsmelbas  22374  madetsmelbas2  22375  mdetleib2  22498  mdetf  22505  mdetdiaglem  22508  mdetdiag  22509  mdetdiagid  22510  mdetrlin  22512  mdetrsca  22513  mdetralt  22518  mdetuni0  22531  smadiadetlem4  22579  chpscmat  22752  chp0mat  22756  chpidmat  22757  amgmlem  26922  amgm  26923  wilthlem2  27001  wilthlem3  27002  lgseisenlem3  27310  lgseisenlem4  27311  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  rlocaddval  33227  rlocmulval  33228  rloccring  33229  unitprodclb  33346  cringm4  33403  rprmdvdsprod  33491  1arithidomlem1  33492  1arithidom  33494  1arithufdlem3  33503  dfufd2lem  33506  mdetpmtr1  33828  aks6d1c1p2  42142  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p7  42146  aks6d1c1p6  42147  aks6d1c1p8  42148  aks6d1c1  42149  evl1gprodd  42150  aks6d1c2lem3  42159  aks6d1c2lem4  42160  idomnnzgmulnz  42166  aks6d1c5lem0  42168  aks6d1c5lem3  42170  aks6d1c5lem2  42171  aks6d1c5  42172  deg1gprod  42173  aks6d1c6lem2  42204  aks6d1c6lem3  42205  aks6d1c6lem4  42206  aks6d1c6lem5  42210  aks5lem2  42220  aks5lem3a  42222  unitscyglem5  42232  pwsgprod  42577  evlsvvvallem  42594  selvvvval  42618  evlselv  42620  mhphf  42630  mgpsumunsn  48392  mgpsumz  48393  mgpsumn  48394  amgmwlem  49834  amgmlemALT  49835