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

Theorem cmnmnd 18189
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 2620 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2620 . . 3 (+g𝐺) = (+g𝐺)
31, 2iscmn 18181 . 2 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥)))
43simplbi 476 1 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  wral 2909  cfv 5876  (class class class)co 6635  Basecbs 15838  +gcplusg 15922  Mndcmnd 17275  CMndccmn 18174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-cmn 18176
This theorem is referenced by:  cmn32  18192  cmn4  18193  cmn12  18194  mulgnn0di  18212  mulgmhm  18214  ghmcmn  18218  prdscmnd  18245  gsumres  18295  gsumcl2  18296  gsumf1o  18298  gsumsubmcl  18300  gsumadd  18304  gsumsplit  18309  gsummhm  18319  gsummulglem  18322  gsuminv  18327  gsumunsnfd  18337  gsumdifsnd  18341  gsum2d  18352  prdsgsum  18358  srgmnd  18490  gsumvsmul  18908  psrbagev1  19491  evlslem3  19495  evlslem1  19496  frlmgsum  20092  frlmup2  20119  islindf4  20158  mdetdiagid  20387  mdetrlin  20389  mdetrsca  20390  gsummatr01lem3  20444  gsummatr01  20446  chpscmat  20628  chp0mat  20632  chpidmat  20633  tmdgsum  21880  tmdgsum2  21881  tsms0  21926  tsmsmhm  21930  tsmsadd  21931  tgptsmscls  21934  tsmssplit  21936  tsmsxplem1  21937  tsmsxplem2  21938  imasdsf1olem  22159  lgseisenlem4  25084  xrge00  29660  xrge0omnd  29685  slmdmnd  29733  gsumle  29753  gsummptres  29758  xrge0iifmhm  29959  xrge0tmdOLD  29965  esum0  30085  esumsnf  30100  esumcocn  30116  gsumge0cl  40351  sge0tsms  40360  gsumpr  41904  gsumdifsndf  41909
  Copyright terms: Public domain W3C validator