Theorem crngmgp 20460

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  CMndccmn 19987  mulGrpcmgp 20353  Ringcrg 20452  CRingccrg 20453

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-cring 20455

This theorem is used by:  crngcom  20471  crngbascntr  20476  gsummgp0  20540  prdscrngd  20544  pwsgprod  20552  crngbinom  20558  unitabl  20607  subrgcrng  20820  cringm4  21620  frobrhm  21874  mplbas2  22344  evlslem3  22382  evlslem6  22383  evlslem1  22384  evlsvvvallem  22393  evlsgsummul  22399  selvvvval  22444  evls1gsummul  22636  evl1gsummul  22671  mamuvs2  22714  matgsumcl  22768  madetsmelbas  22772  madetsmelbas2  22773  mdetleib2  22896  mdetf  22903  mdetdiaglem  22906  mdetdiag  22907  mdetdiagid  22908  mdetrlin  22910  mdetrsca  22911  mdetralt  22916  mdetuni0  22929  smadiadetlem4  22977  chpscmat  23153  chp0mat  23157  chpidmat  23158  amgmlem  27310  amgm  27311  wilthlem2  27389  wilthlem3  27390  lgseisenlem3  27697  lgseisenlem4  27698  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  rlocaddval  33823  rlocmulval  33824  rloccring  33825  domnprodeq0  33833  unitprodclb  33937  rprmdvdsprod  34059  1arithidomlem1  34060  1arithidom  34062  1arithufdlem3  34071  dfufd2lem  34074  deg1prod  34108  evlextv  34167  psrmonprod  34177  vietalem  34204  mdetpmtr1  34448  aks6d1c1p2  43139  aks6d1c1p3  43140  aks6d1c1p4  43141  aks6d1c1p5  43142  aks6d1c1p7  43143  aks6d1c1p6  43144  aks6d1c1p8  43145  aks6d1c1  43146  evl1gprodd  43147  aks6d1c2lem3  43156  aks6d1c2lem4  43157  idomnnzgmulnz  43163  aks6d1c5lem0  43165  aks6d1c5lem3  43167  aks6d1c5lem2  43168  aks6d1c5  43169  deg1gprod  43170  aks6d1c6lem2  43201  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6lem5  43207  aks5lem2  43217  aks5lem3a  43219  unitscyglem5  43229  evlselv  43597  mhphf  43605  mgpsumunsn  49442  mgpsumz  49443  mgpsumn  49444  amgmwlem  50956  amgmlemALT  50957