Theorem crngmgp 20188

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  CMndccmn 19721  mulGrpcmgp 20087  Ringcrg 20180  CRingccrg 20181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-cring 20183

This theorem is referenced by:  crngcom  20198  crngbascntr  20203  gsummgp0  20265  prdscrngd  20269  pwsgprod  20277  crngbinom  20283  unitabl  20332  subrgcrng  20520  frobrhm  21542  sraassaOLD  21837  mplbas2  22009  evlslem3  22047  evlslem6  22048  evlslem1  22049  evlsvvvallem  22058  evlsgsummul  22064  evls1gsummul  22281  evl1gsummul  22316  mamuvs2  22362  matgsumcl  22416  madetsmelbas  22420  madetsmelbas2  22421  mdetleib2  22544  mdetf  22551  mdetdiaglem  22554  mdetdiag  22555  mdetdiagid  22556  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  mdetuni0  22577  smadiadetlem4  22625  chpscmat  22798  chp0mat  22802  chpidmat  22803  amgmlem  26968  amgm  26969  wilthlem2  27047  wilthlem3  27048  lgseisenlem3  27356  lgseisenlem4  27357  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  rlocaddval  33362  rlocmulval  33363  rloccring  33364  domnprodeq0  33370  unitprodclb  33482  cringm4  33539  rprmdvdsprod  33627  1arithidomlem1  33628  1arithidom  33630  1arithufdlem3  33639  dfufd2lem  33642  deg1prod  33676  evlextv  33719  psrmonprod  33729  vietalem  33756  mdetpmtr1  34001  aks6d1c1p2  42479  aks6d1c1p3  42480  aks6d1c1p4  42481  aks6d1c1p5  42482  aks6d1c1p7  42483  aks6d1c1p6  42484  aks6d1c1p8  42485  aks6d1c1  42486  evl1gprodd  42487  aks6d1c2lem3  42496  aks6d1c2lem4  42497  idomnnzgmulnz  42503  aks6d1c5lem0  42505  aks6d1c5lem3  42507  aks6d1c5lem2  42508  aks6d1c5  42509  deg1gprod  42510  aks6d1c6lem2  42541  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c6lem5  42547  aks5lem2  42557  aks5lem3a  42559  unitscyglem5  42569  selvvvval  42943  evlselv  42945  mhphf  42955  mgpsumunsn  48721  mgpsumz  48722  mgpsumn  48723  amgmwlem  50161  amgmlemALT  50162