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

Theorem cmnmnd 18851
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 2818 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2818 . . 3 (+g𝐺) = (+g𝐺)
31, 2iscmn 18843 . 2 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥)))
43simplbi 498 1 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  wral 3135  cfv 6348  (class class class)co 7145  Basecbs 16471  +gcplusg 16553  Mndcmnd 17899  CMndccmn 18835
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-ral 3140  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-ov 7148  df-cmn 18837
This theorem is referenced by:  cmn32  18854  cmn4  18855  cmn12  18856  rinvmod  18858  mulgnn0di  18875  mulgmhm  18877  ghmcmn  18881  prdscmnd  18910  gsumres  18962  gsumcl2  18963  gsumf1o  18965  gsumsubmcl  18968  gsumadd  18972  gsumsplit  18977  gsummhm  18987  gsummulglem  18990  gsuminv  18995  gsumpr  19004  gsumunsnfd  19006  gsumdifsnd  19010  gsum2d  19021  prdsgsum  19030  srgmnd  19188  gsumvsmul  19627  psrbagev1  20218  evlslem3  20221  evlslem1  20223  frlmgsum  20844  frlmup2  20871  islindf4  20910  mdetdiagid  21137  mdetrlin  21139  mdetrsca  21140  gsummatr01lem3  21194  gsummatr01  21196  chpscmat  21378  chp0mat  21382  chpidmat  21383  tmdgsum  22631  tmdgsum2  22632  tsms0  22677  tsmsmhm  22681  tsmsadd  22682  tgptsmscls  22685  tsmssplit  22687  tsmsxplem1  22688  tsmsxplem2  22689  imasdsf1olem  22910  lgseisenlem4  25881  xrge00  30600  gsumvsmul1  30616  gsummptres  30617  xrge0omnd  30639  gsumle  30652  slmdmnd  30761  lbsdiflsp0  30921  xrge0iifmhm  31081  xrge0tmdALT  31088  esum0  31207  esumsnf  31222  esumcocn  31238  gsumge0cl  42530  sge0tsms  42539  gsumdifsndf  43965
  Copyright terms: Public domain W3C validator