Theorem crngmgp 20367

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ‘cfv 6540  CMndccmn 19894  mulGrpcmgp 20260  Ringcrg 20359  CRingccrg 20360

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-cring 20362

This theorem is used by:  crngcom  20377  crngbascntr  20382  gsummgp0  20445  prdscrngd  20449  pwsgprod  20457  crngbinom  20463  unitabl  20512  subrgcrng  20724  cringm4  21521  frobrhm  21775  mplbas2  22243  evlslem3  22281  evlslem6  22282  evlslem1  22283  evlsvvvallem  22292  evlsgsummul  22298  selvvvval  22343  evls1gsummul  22535  evl1gsummul  22570  mamuvs2  22613  matgsumcl  22667  madetsmelbas  22671  madetsmelbas2  22672  mdetleib2  22795  mdetf  22802  mdetdiaglem  22805  mdetdiag  22806  mdetdiagid  22807  mdetrlin  22809  mdetrsca  22810  mdetralt  22815  mdetuni0  22828  smadiadetlem4  22876  chpscmat  23049  chp0mat  23053  chpidmat  23054  amgmlem  27205  amgm  27206  wilthlem2  27284  wilthlem3  27285  lgseisenlem3  27592  lgseisenlem4  27593  elrgspnsubrunlem1  33631  elrgspnsubrunlem2  33632  rlocaddval  33653  rlocmulval  33654  rloccring  33655  domnprodeq0  33663  unitprodclb  33766  rprmdvdsprod  33888  1arithidomlem1  33889  1arithidom  33891  1arithufdlem3  33900  dfufd2lem  33903  deg1prod  33937  evlextv  33996  psrmonprod  34006  vietalem  34033  mdetpmtr1  34277  aks6d1c1p2  42934  aks6d1c1p3  42935  aks6d1c1p4  42936  aks6d1c1p5  42937  aks6d1c1p7  42938  aks6d1c1p6  42939  aks6d1c1p8  42940  aks6d1c1  42941  evl1gprodd  42942  aks6d1c2lem3  42951  aks6d1c2lem4  42952  idomnnzgmulnz  42958  aks6d1c5lem0  42960  aks6d1c5lem3  42962  aks6d1c5lem2  42963  aks6d1c5  42964  deg1gprod  42965  aks6d1c6lem2  42996  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c6lem5  43002  aks5lem2  43012  aks5lem3a  43014  unitscyglem5  43024  evlselv  43379  mhphf  43387  mgpsumunsn  49198  mgpsumz  49199  mgpsumn  49200  amgmwlem  50707  amgmlemALT  50708