Theorem crngmgp 20319

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ‘cfv 6534  CMndccmn 19846  mulGrpcmgp 20212  Ringcrg 20311  CRingccrg 20312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6490  df-fv 6542  df-cring 20314

This theorem is referenced by:  crngcom  20329  crngbascntr  20334  gsummgp0  20395  prdscrngd  20399  pwsgprod  20407  crngbinom  20413  unitabl  20462  subrgcrng  20656  cringm4  21438  frobrhm  21690  mplbas2  22158  evlslem3  22196  evlslem6  22197  evlslem1  22198  evlsvvvallem  22207  evlsgsummul  22213  selvvvval  22258  evls1gsummul  22450  evl1gsummul  22485  mamuvs2  22528  matgsumcl  22582  madetsmelbas  22586  madetsmelbas2  22587  mdetleib2  22710  mdetf  22717  mdetdiaglem  22720  mdetdiag  22721  mdetdiagid  22722  mdetrlin  22724  mdetrsca  22725  mdetralt  22730  mdetuni0  22743  smadiadetlem4  22791  chpscmat  22964  chp0mat  22968  chpidmat  22969  amgmlem  27116  amgm  27117  wilthlem2  27195  wilthlem3  27196  lgseisenlem3  27503  lgseisenlem4  27504  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  rlocaddval  33526  rlocmulval  33527  rloccring  33528  domnprodeq0  33536  unitprodclb  33642  rprmdvdsprod  33765  1arithidomlem1  33766  1arithidom  33768  1arithufdlem3  33777  dfufd2lem  33780  deg1prod  33814  evlextv  33873  psrmonprod  33883  vietalem  33910  mdetpmtr1  34154  aks6d1c1p2  42761  aks6d1c1p3  42762  aks6d1c1p4  42763  aks6d1c1p5  42764  aks6d1c1p7  42765  aks6d1c1p6  42766  aks6d1c1p8  42767  aks6d1c1  42768  evl1gprodd  42769  aks6d1c2lem3  42778  aks6d1c2lem4  42779  idomnnzgmulnz  42785  aks6d1c5lem0  42787  aks6d1c5lem3  42789  aks6d1c5lem2  42790  aks6d1c5  42791  deg1gprod  42792  aks6d1c6lem2  42823  aks6d1c6lem3  42824  aks6d1c6lem4  42825  aks6d1c6lem5  42829  aks5lem2  42839  aks5lem3a  42841  unitscyglem5  42851  evlselv  43208  mhphf  43216  mgpsumunsn  49021  mgpsumz  49022  mgpsumn  49023  amgmwlem  50471  amgmlemALT  50472