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

Theorem cmnmnd 18522
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 2800 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2800 . . 3 (+g𝐺) = (+g𝐺)
31, 2iscmn 18514 . 2 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)(𝑥(+g𝐺)𝑦) = (𝑦(+g𝐺)𝑥)))
43simplbi 492 1 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  wral 3090  cfv 6102  (class class class)co 6879  Basecbs 16183  +gcplusg 16266  Mndcmnd 17608  CMndccmn 18507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-br 4845  df-iota 6065  df-fv 6110  df-ov 6882  df-cmn 18509
This theorem is referenced by:  cmn32  18525  cmn4  18526  cmn12  18527  mulgnn0di  18545  mulgmhm  18547  ghmcmn  18551  prdscmnd  18578  gsumres  18628  gsumcl2  18629  gsumf1o  18631  gsumsubmcl  18633  gsumadd  18637  gsumsplit  18642  gsummhm  18652  gsummulglem  18655  gsuminv  18660  gsumunsnfd  18670  gsumdifsnd  18674  gsum2d  18685  prdsgsum  18691  srgmnd  18824  gsumvsmul  19244  psrbagev1  19831  evlslem3  19835  evlslem1  19836  frlmgsum  20435  frlmup2  20462  islindf4  20501  mdetdiagid  20731  mdetrlin  20733  mdetrsca  20734  gsummatr01lem3  20789  gsummatr01  20791  chpscmat  20974  chp0mat  20978  chpidmat  20979  tmdgsum  22226  tmdgsum2  22227  tsms0  22272  tsmsmhm  22276  tsmsadd  22277  tgptsmscls  22280  tsmssplit  22282  tsmsxplem1  22283  tsmsxplem2  22284  imasdsf1olem  22505  lgseisenlem4  25454  xrge00  30201  xrge0omnd  30226  slmdmnd  30274  gsumle  30294  gsummptres  30299  xrge0iifmhm  30500  xrge0tmdOLD  30506  esum0  30626  esumsnf  30641  esumcocn  30657  gsumge0cl  41326  sge0tsms  41335  gsumpr  42933  gsumdifsndf  42938
  Copyright terms: Public domain W3C validator