Theorem crngmgp 20380

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  CMndccmn 19907  mulGrpcmgp 20273  Ringcrg 20372  CRingccrg 20373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-cring 20375

This theorem is used by:  crngcom  20390  crngbascntr  20395  gsummgp0  20458  prdscrngd  20462  pwsgprod  20470  crngbinom  20476  unitabl  20525  subrgcrng  20737  cringm4  21534  frobrhm  21788  mplbas2  22258  evlslem3  22296  evlslem6  22297  evlslem1  22298  evlsvvvallem  22307  evlsgsummul  22313  selvvvval  22358  evls1gsummul  22550  evl1gsummul  22585  mamuvs2  22628  matgsumcl  22682  madetsmelbas  22686  madetsmelbas2  22687  mdetleib2  22810  mdetf  22817  mdetdiaglem  22820  mdetdiag  22821  mdetdiagid  22822  mdetrlin  22824  mdetrsca  22825  mdetralt  22830  mdetuni0  22843  smadiadetlem4  22891  chpscmat  23067  chp0mat  23071  chpidmat  23072  amgmlem  27226  amgm  27227  wilthlem2  27305  wilthlem3  27306  lgseisenlem3  27613  lgseisenlem4  27614  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  rlocaddval  33709  rlocmulval  33710  rloccring  33711  domnprodeq0  33719  unitprodclb  33822  rprmdvdsprod  33944  1arithidomlem1  33945  1arithidom  33947  1arithufdlem3  33956  dfufd2lem  33959  deg1prod  33993  evlextv  34052  psrmonprod  34062  vietalem  34089  mdetpmtr1  34333  aks6d1c1p2  42975  aks6d1c1p3  42976  aks6d1c1p4  42977  aks6d1c1p5  42978  aks6d1c1p7  42979  aks6d1c1p6  42980  aks6d1c1p8  42981  aks6d1c1  42982  evl1gprodd  42983  aks6d1c2lem3  42992  aks6d1c2lem4  42993  idomnnzgmulnz  42999  aks6d1c5lem0  43001  aks6d1c5lem3  43003  aks6d1c5lem2  43004  aks6d1c5  43005  deg1gprod  43006  aks6d1c6lem2  43037  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6lem5  43043  aks5lem2  43053  aks5lem3a  43055  unitscyglem5  43065  evlselv  43435  mhphf  43443  mgpsumunsn  49291  mgpsumz  49292  mgpsumn  49293  amgmwlem  50820  amgmlemALT  50821