Theorem crngmgp 20518

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6566  CMndccmn 20045  mulGrpcmgp 20411  Ringcrg 20510  CRingccrg 20511

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-cring 20513

This theorem is used by:  crngcom  20529  crngbascntr  20534  gsummgp0  20598  prdscrngd  20602  pwsgprod  20610  crngbinom  20616  unitabl  20665  subrgcrng  20878  cringm4  21678  frobrhm  21936  mplbas2  22406  evlslem3  22444  evlslem6  22445  evlslem1  22446  evlsvvvallem  22455  evlsgsummul  22461  selvvvval  22506  evls1gsummul  22698  evl1gsummul  22733  mamuvs2  22776  matgsumcl  22830  madetsmelbas  22834  madetsmelbas2  22835  mdetleib2  22958  mdetf  22965  mdetdiaglem  22968  mdetdiag  22969  mdetdiagid  22970  mdetrlin  22972  mdetrsca  22973  mdetralt  22978  mdetuni0  22991  smadiadetlem4  23039  chpscmat  23215  chp0mat  23219  chpidmat  23220  amgmlem  27374  amgm  27375  wilthlem2  27453  wilthlem3  27454  lgseisenlem3  27761  lgseisenlem4  27762  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  rlocaddval  33929  rlocmulval  33930  rloccring  33931  domnprodeq0  33939  unitprodclb  34048  rprmdvdsprod  34170  1arithidomlem1  34171  1arithidom  34173  1arithufdlem3  34182  dfufd2lem  34185  deg1prod  34218  evlextv  34285  psrmonprod  34295  vietalem  34322  mdetpmtr1  34566  aks6d1c1p2  43425  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1p7  43429  aks6d1c1p6  43430  aks6d1c1p8  43431  aks6d1c1  43432  evl1gprodd  43433  aks6d1c2lem3  43442  aks6d1c2lem4  43443  idomnnzgmulnz  43449  aks6d1c5lem0  43451  aks6d1c5lem3  43453  aks6d1c5lem2  43454  aks6d1c5  43455  deg1gprod  43456  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c6lem5  43493  aks5lem2  43503  aks5lem3a  43505  unitscyglem5  43515  evlselv  43883  mhphf  43891  mgpsumunsn  49804  mgpsumz  49805  mgpsumn  49806  amgmwlem  51415  amgmlemALT  51416