Theorem crngmgp 18775

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  ‘cfv 6049  CMndccmn 18413  mulGrpcmgp 18709  Ringcrg 18767  CRingccrg 18768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-cring 18770

This theorem is referenced by:  crngcom  18782  gsummgp0  18828  prdscrngd  18833  crngbinom  18841  unitabl  18888  subrgcrng  19006  sraassa  19547  mplbas2  19692  evlslem6  19735  evlslem3  19736  evlslem1  19737  evls1gsummul  19912  evl1gsummul  19946  mamuvs2  20434  matgsumcl  20488  madetsmelbas  20492  madetsmelbas2  20493  mdetleib2  20616  mdetf  20623  mdetdiaglem  20626  mdetdiag  20627  mdetdiagid  20628  mdetrlin  20630  mdetrsca  20631  mdetralt  20636  mdetuni0  20649  smadiadetlem4  20697  chpscmat  20869  chp0mat  20873  chpidmat  20874  amgmlem  24936  amgm  24937  wilthlem2  25015  wilthlem3  25016  lgseisenlem3  25322  lgseisenlem4  25323  mdetpmtr1  30219  mgpsumunsn  42668  mgpsumz  42669  mgpsumn  42670  amgmwlem  43079  amgmlemALT  43080