Theorem crngmgp 20206

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  CMndccmn 19766  mulGrpcmgp 20105  Ringcrg 20198  CRingccrg 20199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-cring 20201

This theorem is referenced by:  crngcom  20216  crngbascntr  20221  gsummgp0  20283  prdscrngd  20287  crngbinom  20300  unitabl  20349  subrgcrng  20540  frobrhm  21541  sraassaOLD  21835  mplbas2  22005  evlslem3  22043  evlslem6  22044  evlslem1  22045  evlsgsummul  22055  evls1gsummul  22268  evl1gsummul  22303  mamuvs2  22349  matgsumcl  22403  madetsmelbas  22407  madetsmelbas2  22408  mdetleib2  22531  mdetf  22538  mdetdiaglem  22541  mdetdiag  22542  mdetdiagid  22543  mdetrlin  22545  mdetrsca  22546  mdetralt  22551  mdetuni0  22564  smadiadetlem4  22612  chpscmat  22785  chp0mat  22789  chpidmat  22790  amgmlem  26957  amgm  26958  wilthlem2  27036  wilthlem3  27037  lgseisenlem3  27345  lgseisenlem4  27346  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  rlocaddval  33268  rlocmulval  33269  rloccring  33270  unitprodclb  33409  cringm4  33466  rprmdvdsprod  33554  1arithidomlem1  33555  1arithidom  33557  1arithufdlem3  33566  dfufd2lem  33569  mdetpmtr1  33859  aks6d1c1p2  42127  aks6d1c1p3  42128  aks6d1c1p4  42129  aks6d1c1p5  42130  aks6d1c1p7  42131  aks6d1c1p6  42132  aks6d1c1p8  42133  aks6d1c1  42134  evl1gprodd  42135  aks6d1c2lem3  42144  aks6d1c2lem4  42145  idomnnzgmulnz  42151  aks6d1c5lem0  42153  aks6d1c5lem3  42155  aks6d1c5lem2  42156  aks6d1c5  42157  deg1gprod  42158  aks6d1c6lem2  42189  aks6d1c6lem3  42190  aks6d1c6lem4  42191  aks6d1c6lem5  42195  aks5lem2  42205  aks5lem3a  42207  unitscyglem5  42217  pwsgprod  42542  evlsvvvallem  42559  selvvvval  42583  evlselv  42585  mhphf  42595  mgpsumunsn  48316  mgpsumz  48317  mgpsumn  48318  amgmwlem  49646  amgmlemALT  49647