Theorem crngmgp 20278

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ‘cfv 6516  CMndccmn 19811  mulGrpcmgp 20177  Ringcrg 20270  CRingccrg 20271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-cring 20273

This theorem is referenced by:  crngcom  20288  crngbascntr  20293  gsummgp0  20353  prdscrngd  20357  pwsgprod  20365  crngbinom  20371  unitabl  20420  subrgcrng  20612  frobrhm  21615  mplbas2  22083  evlslem3  22121  evlslem6  22122  evlslem1  22123  evlsvvvallem  22132  evlsgsummul  22138  selvvvval  22183  evls1gsummul  22376  evl1gsummul  22411  mamuvs2  22454  matgsumcl  22508  madetsmelbas  22512  madetsmelbas2  22513  mdetleib2  22636  mdetf  22643  mdetdiaglem  22646  mdetdiag  22647  mdetdiagid  22648  mdetrlin  22650  mdetrsca  22651  mdetralt  22656  mdetuni0  22669  smadiadetlem4  22717  chpscmat  22890  chp0mat  22894  chpidmat  22895  amgmlem  27042  amgm  27043  wilthlem2  27121  wilthlem3  27122  lgseisenlem3  27429  lgseisenlem4  27430  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  rlocaddval  33411  rlocmulval  33412  rloccring  33413  domnprodeq0  33421  unitprodclb  33536  cringm4  33593  rprmdvdsprod  33691  1arithidomlem1  33692  1arithidom  33694  1arithufdlem3  33703  dfufd2lem  33706  deg1prod  33740  evlextv  33800  psrmonprod  33810  vietalem  33837  mdetpmtr1  34081  aks6d1c1p2  42687  aks6d1c1p3  42688  aks6d1c1p4  42689  aks6d1c1p5  42690  aks6d1c1p7  42691  aks6d1c1p6  42692  aks6d1c1p8  42693  aks6d1c1  42694  evl1gprodd  42695  aks6d1c2lem3  42704  aks6d1c2lem4  42705  idomnnzgmulnz  42711  aks6d1c5lem0  42713  aks6d1c5lem3  42715  aks6d1c5lem2  42716  aks6d1c5  42717  deg1gprod  42718  aks6d1c6lem2  42749  aks6d1c6lem3  42750  aks6d1c6lem4  42751  aks6d1c6lem5  42755  aks5lem2  42765  aks5lem3a  42767  unitscyglem5  42777  evlselv  43132  mhphf  43140  mgpsumunsn  48944  mgpsumz  48945  mgpsumn  48946  amgmwlem  50384  amgmlemALT  50385