Theorem crngmgp 20213

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  CMndccmn 19746  mulGrpcmgp 20112  Ringcrg 20205  CRingccrg 20206

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-cring 20208

This theorem is referenced by:  crngcom  20223  crngbascntr  20228  gsummgp0  20288  prdscrngd  20292  pwsgprod  20300  crngbinom  20306  unitabl  20355  subrgcrng  20543  frobrhm  21565  mplbas2  22030  evlslem3  22068  evlslem6  22069  evlslem1  22070  evlsvvvallem  22079  evlsgsummul  22085  evls1gsummul  22300  evl1gsummul  22335  mamuvs2  22381  matgsumcl  22435  madetsmelbas  22439  madetsmelbas2  22440  mdetleib2  22563  mdetf  22570  mdetdiaglem  22573  mdetdiag  22574  mdetdiagid  22575  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetuni0  22596  smadiadetlem4  22644  chpscmat  22817  chp0mat  22821  chpidmat  22822  amgmlem  26967  amgm  26968  wilthlem2  27046  wilthlem3  27047  lgseisenlem3  27354  lgseisenlem4  27355  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  rlocaddval  33344  rlocmulval  33345  rloccring  33346  domnprodeq0  33352  unitprodclb  33464  cringm4  33521  rprmdvdsprod  33609  1arithidomlem1  33610  1arithidom  33612  1arithufdlem3  33621  dfufd2lem  33624  deg1prod  33658  evlextv  33701  psrmonprod  33711  vietalem  33738  mdetpmtr1  33983  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1p8  42568  aks6d1c1  42569  evl1gprodd  42570  aks6d1c2lem3  42579  aks6d1c2lem4  42580  idomnnzgmulnz  42586  aks6d1c5lem0  42588  aks6d1c5lem3  42590  aks6d1c5lem2  42591  aks6d1c5  42592  deg1gprod  42593  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6lem5  42630  aks5lem2  42640  aks5lem3a  42642  unitscyglem5  42652  selvvvval  43032  evlselv  43034  mhphf  43044  mgpsumunsn  48849  mgpsumz  48850  mgpsumn  48851  amgmwlem  50289  amgmlemALT  50290