Theorem crngmgp 20213

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  CMndccmn 19746  mulGrpcmgp 20112  Ringcrg 20205  CRingccrg 20206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-cring 20208

This theorem is referenced by:  crngcom  20223  crngbascntr  20228  gsummgp0  20288  prdscrngd  20292  pwsgprod  20300  crngbinom  20306  unitabl  20355  subrgcrng  20547  frobrhm  21550  mplbas2  22018  evlslem3  22056  evlslem6  22057  evlslem1  22058  evlsvvvallem  22067  evlsgsummul  22073  selvvvval  22118  evls1gsummul  22311  evl1gsummul  22346  mamuvs2  22389  matgsumcl  22443  madetsmelbas  22447  madetsmelbas2  22448  mdetleib2  22571  mdetf  22578  mdetdiaglem  22581  mdetdiag  22582  mdetdiagid  22583  mdetrlin  22585  mdetrsca  22586  mdetralt  22591  mdetuni0  22604  smadiadetlem4  22652  chpscmat  22825  chp0mat  22829  chpidmat  22830  amgmlem  26971  amgm  26972  wilthlem2  27050  wilthlem3  27051  lgseisenlem3  27358  lgseisenlem4  27359  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  rlocaddval  33349  rlocmulval  33350  rloccring  33351  domnprodeq0  33357  unitprodclb  33472  cringm4  33529  rprmdvdsprod  33617  1arithidomlem1  33618  1arithidom  33620  1arithufdlem3  33629  dfufd2lem  33632  deg1prod  33666  evlextv  33726  psrmonprod  33736  vietalem  33763  mdetpmtr1  34007  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  aks6d1c1p6  42599  aks6d1c1p8  42600  aks6d1c1  42601  evl1gprodd  42602  aks6d1c2lem3  42611  aks6d1c2lem4  42612  idomnnzgmulnz  42618  aks6d1c5lem0  42620  aks6d1c5lem3  42622  aks6d1c5lem2  42623  aks6d1c5  42624  deg1gprod  42625  aks6d1c6lem2  42656  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6lem5  42662  aks5lem2  42672  aks5lem3a  42674  unitscyglem5  42684  evlselv  43039  mhphf  43047  mgpsumunsn  48852  mgpsumz  48853  mgpsumn  48854  amgmwlem  50292  amgmlemALT  50293