Theorem crngmgp 20474

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6541  CMndccmn 20001  mulGrpcmgp 20367  Ringcrg 20466  CRingccrg 20467

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549  df-cring 20469

This theorem is used by:  crngcom  20485  crngbascntr  20490  gsummgp0  20554  prdscrngd  20558  pwsgprod  20566  crngbinom  20572  unitabl  20621  subrgcrng  20834  cringm4  21634  frobrhm  21888  mplbas2  22358  evlslem3  22396  evlslem6  22397  evlslem1  22398  evlsvvvallem  22407  evlsgsummul  22413  selvvvval  22458  evls1gsummul  22650  evl1gsummul  22685  mamuvs2  22728  matgsumcl  22782  madetsmelbas  22786  madetsmelbas2  22787  mdetleib2  22910  mdetf  22917  mdetdiaglem  22920  mdetdiag  22921  mdetdiagid  22922  mdetrlin  22924  mdetrsca  22925  mdetralt  22930  mdetuni0  22943  smadiadetlem4  22991  chpscmat  23167  chp0mat  23171  chpidmat  23172  amgmlem  27324  amgm  27325  wilthlem2  27403  wilthlem3  27404  lgseisenlem3  27711  lgseisenlem4  27712  elrgspnsubrunlem1  33856  elrgspnsubrunlem2  33857  rlocaddval  33878  rlocmulval  33879  rloccring  33880  domnprodeq0  33888  unitprodclb  33992  rprmdvdsprod  34114  1arithidomlem1  34115  1arithidom  34117  1arithufdlem3  34126  dfufd2lem  34129  deg1prod  34163  evlextv  34222  psrmonprod  34232  vietalem  34259  mdetpmtr1  34503  aks6d1c1p2  43266  aks6d1c1p3  43267  aks6d1c1p4  43268  aks6d1c1p5  43269  aks6d1c1p7  43270  aks6d1c1p6  43271  aks6d1c1p8  43272  aks6d1c1  43273  evl1gprodd  43274  aks6d1c2lem3  43283  aks6d1c2lem4  43284  idomnnzgmulnz  43290  aks6d1c5lem0  43292  aks6d1c5lem3  43294  aks6d1c5lem2  43295  aks6d1c5  43296  deg1gprod  43297  aks6d1c6lem2  43328  aks6d1c6lem3  43329  aks6d1c6lem4  43330  aks6d1c6lem5  43334  aks5lem2  43344  aks5lem3a  43346  unitscyglem5  43356  evlselv  43724  mhphf  43732  mgpsumunsn  49580  mgpsumz  49581  mgpsumn  49582  amgmwlem  51169  amgmlemALT  51170