Theorem crngmgp 20268

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  CMndccmn 19822  mulGrpcmgp 20161  Ringcrg 20260  CRingccrg 20261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-cring 20263

This theorem is referenced by:  crngcom  20278  crngbascntr  20283  gsummgp0  20341  prdscrngd  20345  crngbinom  20358  unitabl  20410  subrgcrng  20603  frobrhm  21617  sraassaOLD  21913  mplbas2  22083  evlslem3  22127  evlslem6  22128  evlslem1  22129  evlsgsummul  22139  evls1gsummul  22350  evl1gsummul  22385  mamuvs2  22431  matgsumcl  22487  madetsmelbas  22491  madetsmelbas2  22492  mdetleib2  22615  mdetf  22622  mdetdiaglem  22625  mdetdiag  22626  mdetdiagid  22627  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  mdetuni0  22648  smadiadetlem4  22696  chpscmat  22869  chp0mat  22873  chpidmat  22874  amgmlem  27051  amgm  27052  wilthlem2  27130  wilthlem3  27131  lgseisenlem3  27439  lgseisenlem4  27440  rlocaddval  33240  rlocmulval  33241  rloccring  33242  unitprodclb  33382  cringm4  33439  rprmdvdsprod  33527  1arithidomlem1  33528  1arithidom  33530  1arithufdlem3  33539  dfufd2lem  33542  mdetpmtr1  33769  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c1  42073  evl1gprodd  42074  aks6d1c2lem3  42083  aks6d1c2lem4  42084  idomnnzgmulnz  42090  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5lem2  42095  aks6d1c5  42096  deg1gprod  42097  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6lem5  42134  aks5lem2  42144  aks5lem3a  42146  unitscyglem5  42156  pwsgprod  42499  evlsvvvallem  42516  selvvvval  42540  evlselv  42542  mhphf  42552  mgpsumunsn  48086  mgpsumz  48087  mgpsumn  48088  amgmwlem  48896  amgmlemALT  48897