Theorem crngmgp 20259

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  CMndccmn 19813  mulGrpcmgp 20152  Ringcrg 20251  CRingccrg 20252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-cring 20254

This theorem is referenced by:  crngcom  20269  crngbascntr  20274  gsummgp0  20332  prdscrngd  20336  crngbinom  20349  unitabl  20401  subrgcrng  20592  frobrhm  21612  sraassaOLD  21908  mplbas2  22078  evlslem3  22122  evlslem6  22123  evlslem1  22124  evlsgsummul  22134  evls1gsummul  22345  evl1gsummul  22380  mamuvs2  22426  matgsumcl  22482  madetsmelbas  22486  madetsmelbas2  22487  mdetleib2  22610  mdetf  22617  mdetdiaglem  22620  mdetdiag  22621  mdetdiagid  22622  mdetrlin  22624  mdetrsca  22625  mdetralt  22630  mdetuni0  22643  smadiadetlem4  22691  chpscmat  22864  chp0mat  22868  chpidmat  22869  amgmlem  27048  amgm  27049  wilthlem2  27127  wilthlem3  27128  lgseisenlem3  27436  lgseisenlem4  27437  rlocaddval  33255  rlocmulval  33256  rloccring  33257  unitprodclb  33397  cringm4  33454  rprmdvdsprod  33542  1arithidomlem1  33543  1arithidom  33545  1arithufdlem3  33554  dfufd2lem  33557  mdetpmtr1  33784  aks6d1c1p2  42091  aks6d1c1p3  42092  aks6d1c1p4  42093  aks6d1c1p5  42094  aks6d1c1p7  42095  aks6d1c1p6  42096  aks6d1c1p8  42097  aks6d1c1  42098  evl1gprodd  42099  aks6d1c2lem3  42108  aks6d1c2lem4  42109  idomnnzgmulnz  42115  aks6d1c5lem0  42117  aks6d1c5lem3  42119  aks6d1c5lem2  42120  aks6d1c5  42121  deg1gprod  42122  aks6d1c6lem2  42153  aks6d1c6lem3  42154  aks6d1c6lem4  42155  aks6d1c6lem5  42159  aks5lem2  42169  aks5lem3a  42171  unitscyglem5  42181  pwsgprod  42531  evlsvvvallem  42548  selvvvval  42572  evlselv  42574  mhphf  42584  mgpsumunsn  48206  mgpsumz  48207  mgpsumn  48208  amgmwlem  49033  amgmlemALT  49034