Theorem crngmgp 20222

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  CMndccmn 19755  mulGrpcmgp 20121  Ringcrg 20214  CRingccrg 20215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-cring 20217

This theorem is referenced by:  crngcom  20232  crngbascntr  20237  gsummgp0  20297  prdscrngd  20301  pwsgprod  20309  crngbinom  20315  unitabl  20364  subrgcrng  20552  frobrhm  21555  mplbas2  22020  evlslem3  22058  evlslem6  22059  evlslem1  22060  evlsvvvallem  22069  evlsgsummul  22075  evls1gsummul  22290  evl1gsummul  22325  mamuvs2  22371  matgsumcl  22425  madetsmelbas  22429  madetsmelbas2  22430  mdetleib2  22553  mdetf  22560  mdetdiaglem  22563  mdetdiag  22564  mdetdiagid  22565  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetuni0  22586  smadiadetlem4  22634  chpscmat  22807  chp0mat  22811  chpidmat  22812  amgmlem  26953  amgm  26954  wilthlem2  27032  wilthlem3  27033  lgseisenlem3  27340  lgseisenlem4  27341  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  rlocaddval  33329  rlocmulval  33330  rloccring  33331  domnprodeq0  33337  unitprodclb  33449  cringm4  33506  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidom  33597  1arithufdlem3  33606  dfufd2lem  33609  deg1prod  33643  evlextv  33686  psrmonprod  33696  vietalem  33723  mdetpmtr1  33967  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c1  42555  evl1gprodd  42556  aks6d1c2lem3  42565  aks6d1c2lem4  42566  idomnnzgmulnz  42572  aks6d1c5lem0  42574  aks6d1c5lem3  42576  aks6d1c5lem2  42577  aks6d1c5  42578  deg1gprod  42579  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6lem5  42616  aks5lem2  42626  aks5lem3a  42628  unitscyglem5  42638  selvvvval  43018  evlselv  43020  mhphf  43030  mgpsumunsn  48837  mgpsumz  48838  mgpsumn  48839  amgmwlem  50277  amgmlemALT  50278