Theorem crngmgp 20167

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  CMndccmn 19700  mulGrpcmgp 20066  Ringcrg 20159  CRingccrg 20160

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-cring 20162

This theorem is referenced by:  crngcom  20177  crngbascntr  20182  gsummgp0  20244  prdscrngd  20248  pwsgprod  20256  crngbinom  20262  unitabl  20311  subrgcrng  20499  frobrhm  21521  sraassaOLD  21816  mplbas2  21988  evlslem3  22026  evlslem6  22027  evlslem1  22028  evlsvvvallem  22037  evlsgsummul  22043  evls1gsummul  22260  evl1gsummul  22295  mamuvs2  22341  matgsumcl  22395  madetsmelbas  22399  madetsmelbas2  22400  mdetleib2  22523  mdetf  22530  mdetdiaglem  22533  mdetdiag  22534  mdetdiagid  22535  mdetrlin  22537  mdetrsca  22538  mdetralt  22543  mdetuni0  22556  smadiadetlem4  22604  chpscmat  22777  chp0mat  22781  chpidmat  22782  amgmlem  26947  amgm  26948  wilthlem2  27026  wilthlem3  27027  lgseisenlem3  27335  lgseisenlem4  27336  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  rlocaddval  33278  rlocmulval  33279  rloccring  33280  domnprodeq0  33286  unitprodclb  33398  cringm4  33455  rprmdvdsprod  33543  1arithidomlem1  33544  1arithidom  33546  1arithufdlem3  33555  dfufd2lem  33558  deg1prod  33592  evlextv  33635  vietalem  33663  mdetpmtr1  33908  aks6d1c1p2  42275  aks6d1c1p3  42276  aks6d1c1p4  42277  aks6d1c1p5  42278  aks6d1c1p7  42279  aks6d1c1p6  42280  aks6d1c1p8  42281  aks6d1c1  42282  evl1gprodd  42283  aks6d1c2lem3  42292  aks6d1c2lem4  42293  idomnnzgmulnz  42299  aks6d1c5lem0  42301  aks6d1c5lem3  42303  aks6d1c5lem2  42304  aks6d1c5  42305  deg1gprod  42306  aks6d1c6lem2  42337  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c6lem5  42343  aks5lem2  42353  aks5lem3a  42355  unitscyglem5  42365  selvvvval  42743  evlselv  42745  mhphf  42755  mgpsumunsn  48523  mgpsumz  48524  mgpsumn  48525  amgmwlem  49963  amgmlemALT  49964