Theorem crngmgp 18942

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  ‘cfv 6135  CMndccmn 18579  mulGrpcmgp 18876  Ringcrg 18934  CRingccrg 18935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-cring 18937

This theorem is referenced by:  crngcom  18949  gsummgp0  18995  prdscrngd  19000  crngbinom  19008  unitabl  19055  subrgcrng  19176  sraassa  19722  mplbas2  19867  evlslem6  19909  evlslem3  19910  evlslem1  19911  evls1gsummul  20086  evl1gsummul  20120  mamuvs2  20616  matgsumcl  20671  madetsmelbas  20675  madetsmelbas2  20676  mdetleib2  20799  mdetf  20806  mdetdiaglem  20809  mdetdiag  20810  mdetdiagid  20811  mdetrlin  20813  mdetrsca  20814  mdetralt  20819  mdetuni0  20832  smadiadetlem4  20881  chpscmat  21054  chp0mat  21058  chpidmat  21059  amgmlem  25168  amgm  25169  wilthlem2  25247  wilthlem3  25248  lgseisenlem3  25554  lgseisenlem4  25555  mdetpmtr1  30487  mgpsumunsn  43155  mgpsumz  43156  mgpsumn  43157  amgmwlem  43654  amgmlemALT  43655