Theorem crngmgp 20126

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  CMndccmn 19686  mulGrpcmgp 20025  Ringcrg 20118  CRingccrg 20119

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-cring 20121

This theorem is referenced by:  crngcom  20136  crngbascntr  20141  gsummgp0  20203  prdscrngd  20207  crngbinom  20220  unitabl  20269  subrgcrng  20460  frobrhm  21461  sraassaOLD  21755  mplbas2  21925  evlslem3  21963  evlslem6  21964  evlslem1  21965  evlsgsummul  21975  evls1gsummul  22188  evl1gsummul  22223  mamuvs2  22269  matgsumcl  22323  madetsmelbas  22327  madetsmelbas2  22328  mdetleib2  22451  mdetf  22458  mdetdiaglem  22461  mdetdiag  22462  mdetdiagid  22463  mdetrlin  22465  mdetrsca  22466  mdetralt  22471  mdetuni0  22484  smadiadetlem4  22532  chpscmat  22705  chp0mat  22709  chpidmat  22710  amgmlem  26876  amgm  26877  wilthlem2  26955  wilthlem3  26956  lgseisenlem3  27264  lgseisenlem4  27265  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  rlocaddval  33192  rlocmulval  33193  rloccring  33194  unitprodclb  33333  cringm4  33390  rprmdvdsprod  33478  1arithidomlem1  33479  1arithidom  33481  1arithufdlem3  33490  dfufd2lem  33493  mdetpmtr1  33786  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1p8  42076  aks6d1c1  42077  evl1gprodd  42078  aks6d1c2lem3  42087  aks6d1c2lem4  42088  idomnnzgmulnz  42094  aks6d1c5lem0  42096  aks6d1c5lem3  42098  aks6d1c5lem2  42099  aks6d1c5  42100  deg1gprod  42101  aks6d1c6lem2  42132  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6lem5  42138  aks5lem2  42148  aks5lem3a  42150  unitscyglem5  42160  pwsgprod  42505  evlsvvvallem  42522  selvvvval  42546  evlselv  42548  mhphf  42558  mgpsumunsn  48322  mgpsumz  48323  mgpsumn  48324  amgmwlem  49764  amgmlemALT  49765