Theorem crngmgp 20383

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 20382	. 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 19910  mulGrpcmgp 20276  Ringcrg 20375  CRingccrg 20376

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 20378

This theorem is used by:  crngcom  20393  crngbascntr  20398  gsummgp0  20461  prdscrngd  20465  pwsgprod  20473  crngbinom  20479  unitabl  20528  subrgcrng  20740  cringm4  21537  frobrhm  21791  mplbas2  22261  evlslem3  22299  evlslem6  22300  evlslem1  22301  evlsvvvallem  22310  evlsgsummul  22316  selvvvval  22361  evls1gsummul  22553  evl1gsummul  22588  mamuvs2  22631  matgsumcl  22685  madetsmelbas  22689  madetsmelbas2  22690  mdetleib2  22813  mdetf  22820  mdetdiaglem  22823  mdetdiag  22824  mdetdiagid  22825  mdetrlin  22827  mdetrsca  22828  mdetralt  22833  mdetuni0  22846  smadiadetlem4  22894  chpscmat  23070  chp0mat  23074  chpidmat  23075  amgmlem  27229  amgm  27230  wilthlem2  27308  wilthlem3  27309  lgseisenlem3  27616  lgseisenlem4  27617  elrgspnsubrunlem1  33690  elrgspnsubrunlem2  33691  rlocaddval  33712  rlocmulval  33713  rloccring  33714  domnprodeq0  33722  unitprodclb  33825  rprmdvdsprod  33947  1arithidomlem1  33948  1arithidom  33950  1arithufdlem3  33959  dfufd2lem  33962  deg1prod  33996  evlextv  34055  psrmonprod  34065  vietalem  34092  mdetpmtr1  34336  aks6d1c1p2  42978  aks6d1c1p3  42979  aks6d1c1p4  42980  aks6d1c1p5  42981  aks6d1c1p7  42982  aks6d1c1p6  42983  aks6d1c1p8  42984  aks6d1c1  42985  evl1gprodd  42986  aks6d1c2lem3  42995  aks6d1c2lem4  42996  idomnnzgmulnz  43002  aks6d1c5lem0  43004  aks6d1c5lem3  43006  aks6d1c5lem2  43007  aks6d1c5  43008  deg1gprod  43009  aks6d1c6lem2  43040  aks6d1c6lem3  43041  aks6d1c6lem4  43042  aks6d1c6lem5  43046  aks5lem2  43056  aks5lem3a  43058  unitscyglem5  43068  evlselv  43438  mhphf  43446  mgpsumunsn  49294  mgpsumz  49295  mgpsumn  49296  amgmwlem  50823  amgmlemALT  50824