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

Theorem cmnmnd 16396
Description: A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
cmnmnd  |-  ( G  e. CMnd  ->  G  e.  Mnd )

Proof of Theorem cmnmnd
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2451 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2451 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
31, 2iscmn 16388 . 2  |-  ( G  e. CMnd 
<->  ( G  e.  Mnd  /\ 
A. x  e.  (
Base `  G ) A. y  e.  ( Base `  G ) ( x ( +g  `  G
) y )  =  ( y ( +g  `  G ) x ) ) )
43simplbi 460 1  |-  ( G  e. CMnd  ->  G  e.  Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   A.wral 2795   ` cfv 5516  (class class class)co 6190   Basecbs 14276   +g cplusg 14340   Mndcmnd 15511  CMndccmn 16381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-cmn 16383
This theorem is referenced by:  cmn32  16399  cmn4  16400  cmn12  16401  mulgnn0di  16417  mulgmhm  16419  prdscmnd  16447  gsumres  16499  gsumcl2  16500  gsumf1o  16502  gsumresOLD  16503  gsumclOLD  16504  gsumf1oOLD  16505  gsumsubmcl  16508  gsumsubmclOLD  16509  gsumadd  16516  gsumaddOLD  16517  gsumsplit  16524  gsumsplitOLD  16525  gsummhm  16537  gsummhmOLD  16538  gsummulglem  16542  gsuminv  16549  gsuminvOLD  16551  gsumunsnd  16557  gsum2d  16568  gsum2dOLD  16569  prdsgsum  16576  prdsgsumOLD  16577  srgmnd  16716  gsumvsmul  17115  gsumvsmulOLD  17116  mplcoe2OLD  17657  psrbagev1  17701  psrbagev1OLD  17702  evlslem3  17707  evlslem1  17708  ply1coeOLD  17856  frlmgsumOLD  18304  frlmgsum  18305  frlmup2  18336  islindf4  18376  mdetdiagid  18522  mdetrlin  18524  mdetrsca  18525  gsummatr01lem3  18579  gsummatr01  18581  tmdgsum  19782  tmdgsum2  19783  tsms0  19831  tsmsmhm  19836  tsmsadd  19837  tgptsmscls  19840  tsmssplit  19842  tsmsxplem1  19843  tsmsxplem2  19844  imasdsf1olem  20064  lgseisenlem4  22807  xrge00  26281  xrge0omnd  26308  slmdmnd  26356  gsumunsnf  26379  gsumle  26380  xrge0iifmhm  26503  xrge0tmdOLD  26509  esum0  26637  esumsn  26649  esumcocn  26663  gsumpr  30896  gsumdifsnd  30900  gsumdifsndf  30903  cpscmat  31296  cp0mat  31300  cpidmat  31301
  Copyright terms: Public domain W3C validator