Theorem crngmgp 20135

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  CMndccmn 19689  mulGrpcmgp 20028  Ringcrg 20127  CRingccrg 20128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-cring 20130

This theorem is referenced by:  crngcom  20145  crngbascntr  20149  gsummgp0  20206  prdscrngd  20210  crngbinom  20223  unitabl  20275  subrgcrng  20465  sraassaOLD  21643  mplbas2  21816  evlslem3  21862  evlslem6  21863  evlslem1  21864  evlsgsummul  21874  evls1gsummul  22064  evl1gsummul  22099  mamuvs2  22126  matgsumcl  22182  madetsmelbas  22186  madetsmelbas2  22187  mdetleib2  22310  mdetf  22317  mdetdiaglem  22320  mdetdiag  22321  mdetdiagid  22322  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  mdetuni0  22343  smadiadetlem4  22391  chpscmat  22564  chp0mat  22568  chpidmat  22569  amgmlem  26730  amgm  26731  wilthlem2  26809  wilthlem3  26810  lgseisenlem3  27116  lgseisenlem4  27117  frobrhm  32652  cringm4  32839  mdetpmtr1  33101  pwsgprod  41416  evlsvvvallem  41435  selvvvval  41459  evlselv  41461  mhphf  41471  mgpsumunsn  47125  mgpsumz  47126  mgpsumn  47127  amgmwlem  47936  amgmlemALT  47937