Theorem crngmgp 18378

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  CMndccmn 18016  mulGrpcmgp 18312  Ringcrg 18370  CRingccrg 18371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-cring 18373

This theorem is referenced by:  crngcom  18385  gsummgp0  18431  prdscrngd  18436  crngbinom  18444  unitabl  18491  subrgcrng  18607  sraassa  19146  mplbas2  19291  evlslem6  19334  evlslem3  19335  evlslem1  19336  evls1gsummul  19511  evl1gsummul  19545  mamuvs2  20031  matgsumcl  20085  madetsmelbas  20089  madetsmelbas2  20090  mdetleib2  20213  mdetf  20220  mdetdiaglem  20223  mdetdiag  20224  mdetdiagid  20225  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  mdetuni0  20246  smadiadetlem4  20294  chpscmat  20466  chp0mat  20470  chpidmat  20471  amgmlem  24516  amgm  24517  wilthlem2  24595  wilthlem3  24596  lgseisenlem3  24902  lgseisenlem4  24903  mdetpmtr1  29217  mgpsumunsn  41933  mgpsumz  41934  mgpsumn  41935  amgmwlem  42357  amgmlemALT  42358