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

Theorem cmnmnd 16285
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 2441 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2441 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
31, 2iscmn 16277 . 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 457 1  |-  ( G  e. CMnd  ->  G  e.  Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761   A.wral 2713   ` cfv 5415  (class class class)co 6090   Basecbs 14170   +g cplusg 14234   Mndcmnd 15405  CMndccmn 16270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093  df-cmn 16272
This theorem is referenced by:  cmn32  16288  cmn4  16289  cmn12  16290  mulgnn0di  16306  mulgmhm  16308  prdscmnd  16336  gsumres  16388  gsumcl2  16389  gsumf1o  16391  gsumresOLD  16392  gsumclOLD  16393  gsumf1oOLD  16394  gsumsubmcl  16397  gsumsubmclOLD  16398  gsumadd  16405  gsumaddOLD  16406  gsumsplit  16413  gsumsplitOLD  16414  gsummhm  16424  gsummhmOLD  16425  gsummulglem  16429  gsuminv  16436  gsuminvOLD  16438  gsumunsnd  16443  gsum2d  16453  gsum2dOLD  16454  prdsgsum  16461  prdsgsumOLD  16462  srgmnd  16601  gsumvsmul  16989  gsumvsmulOLD  16990  mplcoe2  17525  mplcoe2OLD  17526  psrbagev1  17570  psrbagev1OLD  17571  evlslem3  17576  evlslem1  17577  ply1coe  17720  frlmgsumOLD  18154  frlmgsum  18155  frlmup2  18186  islindf4  18226  mdetrlin  18368  mdetrsca  18369  gsummatr01lem3  18422  gsummatr01  18424  tmdgsum  19625  tmdgsum2  19626  tsms0  19674  tsmsmhm  19679  tsmsadd  19680  tgptsmscls  19683  tsmssplit  19685  tsmsxplem1  19686  tsmsxplem2  19687  imasdsf1olem  19907  lgseisenlem4  22650  xrge00  26080  xrge0omnd  26107  slmdmnd  26155  gsumunsnf  26180  gsumle  26181  xrge0iifmhm  26305  xrge0tmdOLD  26311  esum0  26439  esumsn  26451  esumcocn  26465  gsumpr  30675  gsumdifsnd  30679  gsumdifsndf  30682  mdetdiagid  30778
  Copyright terms: Public domain W3C validator