Theorem crngmgp 20318

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  CMndccmn 19845  mulGrpcmgp 20211  Ringcrg 20310  CRingccrg 20311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-cring 20313

This theorem is referenced by:  crngcom  20328  crngbascntr  20333  gsummgp0  20395  prdscrngd  20399  pwsgprod  20407  crngbinom  20413  unitabl  20462  subrgcrng  20674  cringm4  21471  frobrhm  21725  mplbas2  22193  evlslem3  22231  evlslem6  22232  evlslem1  22233  evlsvvvallem  22242  evlsgsummul  22248  selvvvval  22293  evls1gsummul  22485  evl1gsummul  22520  mamuvs2  22563  matgsumcl  22617  madetsmelbas  22621  madetsmelbas2  22622  mdetleib2  22745  mdetf  22752  mdetdiaglem  22755  mdetdiag  22756  mdetdiagid  22757  mdetrlin  22759  mdetrsca  22760  mdetralt  22765  mdetuni0  22778  smadiadetlem4  22826  chpscmat  22999  chp0mat  23003  chpidmat  23004  amgmlem  27154  amgm  27155  wilthlem2  27233  wilthlem3  27234  lgseisenlem3  27541  lgseisenlem4  27542  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  rlocaddval  33589  rlocmulval  33590  rloccring  33591  domnprodeq0  33599  unitprodclb  33702  rprmdvdsprod  33824  1arithidomlem1  33825  1arithidom  33827  1arithufdlem3  33836  dfufd2lem  33839  deg1prod  33873  evlextv  33932  psrmonprod  33942  vietalem  33969  mdetpmtr1  34213  aks6d1c1p2  42876  aks6d1c1p3  42877  aks6d1c1p4  42878  aks6d1c1p5  42879  aks6d1c1p7  42880  aks6d1c1p6  42881  aks6d1c1p8  42882  aks6d1c1  42883  evl1gprodd  42884  aks6d1c2lem3  42893  aks6d1c2lem4  42894  idomnnzgmulnz  42900  aks6d1c5lem0  42902  aks6d1c5lem3  42904  aks6d1c5lem2  42905  aks6d1c5  42906  deg1gprod  42907  aks6d1c6lem2  42938  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c6lem5  42944  aks5lem2  42954  aks5lem3a  42956  unitscyglem5  42966  evlselv  43321  mhphf  43329  mgpsumunsn  49141  mgpsumz  49142  mgpsumn  49143  amgmwlem  50622  amgmlemALT  50623