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

Theorem cmnmnd 17973
Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
cmnmnd (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)

Proof of Theorem cmnmnd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2605 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2605 . . 3 (+g𝐺) = (+g𝐺)
31, 2iscmn 17965 . 2 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥)))
43simplbi 474 1 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  wral 2891  cfv 5786  (class class class)co 6523  Basecbs 15637  +gcplusg 15710  Mndcmnd 17059  CMndccmn 17958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526  df-cmn 17960
This theorem is referenced by:  cmn32  17976  cmn4  17977  cmn12  17978  mulgnn0di  17996  mulgmhm  17998  ghmcmn  18002  prdscmnd  18029  gsumres  18079  gsumcl2  18080  gsumf1o  18082  gsumsubmcl  18084  gsumadd  18088  gsumsplit  18093  gsummhm  18103  gsummulglem  18106  gsuminv  18111  gsumunsnfd  18121  gsumdifsnd  18125  gsum2d  18136  prdsgsum  18142  srgmnd  18274  gsumvsmul  18692  psrbagev1  19273  evlslem3  19277  evlslem1  19278  frlmgsum  19868  frlmup2  19895  islindf4  19934  mdetdiagid  20163  mdetrlin  20165  mdetrsca  20166  gsummatr01lem3  20220  gsummatr01  20222  chpscmat  20404  chp0mat  20408  chpidmat  20409  tmdgsum  21647  tmdgsum2  21648  tsms0  21693  tsmsmhm  21697  tsmsadd  21698  tgptsmscls  21701  tsmssplit  21703  tsmsxplem1  21704  tsmsxplem2  21705  imasdsf1olem  21925  lgseisenlem4  24816  xrge00  28819  xrge0omnd  28844  slmdmnd  28892  gsumle  28912  gsummptres  28917  xrge0iifmhm  29115  xrge0tmdOLD  29121  esum0  29240  esumsnf  29255  esumcocn  29271  gsumge0cl  39064  sge0tsms  39073  gsumpr  41930  gsumdifsndf  41935
  Copyright terms: Public domain W3C validator