MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  crngmgp Structured version   Visualization version   GIF version

Theorem crngmgp 19234
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
StepHypRef Expression
1 ringmgp.g . . 3 𝐺 = (mulGrp‘𝑅)
21iscrng 19233 . 2 (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd))
32simprbi 497 1 (𝑅 ∈ CRing → 𝐺 ∈ CMnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  cfv 6348  CMndccmn 18835  mulGrpcmgp 19168  Ringcrg 19226  CRingccrg 19227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-cring 19229
This theorem is referenced by:  crngcom  19241  gsummgp0  19287  prdscrngd  19292  crngbinom  19300  unitabl  19347  subrgcrng  19468  sraassa  20027  mplbas2  20179  evlslem3  20221  evlslem6  20222  evlslem1  20223  evlsgsummul  20233  evls1gsummul  20416  evl1gsummul  20451  mamuvs2  20943  matgsumcl  20997  madetsmelbas  21001  madetsmelbas2  21002  mdetleib2  21125  mdetf  21132  mdetdiaglem  21135  mdetdiag  21136  mdetdiagid  21137  mdetrlin  21139  mdetrsca  21140  mdetralt  21145  mdetuni0  21158  smadiadetlem4  21206  chpscmat  21378  chp0mat  21382  chpidmat  21383  amgmlem  25494  amgm  25495  wilthlem2  25573  wilthlem3  25574  lgseisenlem3  25880  lgseisenlem4  25881  cringm4  30880  mdetpmtr1  30987  mgpsumunsn  44337  mgpsumz  44338  mgpsumn  44339  amgmwlem  44831  amgmlemALT  44832
  Copyright terms: Public domain W3C validator