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

Theorem cmncom 17028
Description: A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
ablcom.b  |-  B  =  ( Base `  G
)
ablcom.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
cmncom  |-  ( ( G  e. CMnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  =  ( Y  .+  X
) )

Proof of Theorem cmncom
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ablcom.b . . . . . 6  |-  B  =  ( Base `  G
)
2 ablcom.p . . . . . 6  |-  .+  =  ( +g  `  G )
31, 2iscmn 17019 . . . . 5  |-  ( G  e. CMnd 
<->  ( G  e.  Mnd  /\ 
A. x  e.  B  A. y  e.  B  ( x  .+  y )  =  ( y  .+  x ) ) )
43simprbi 462 . . . 4  |-  ( G  e. CMnd  ->  A. x  e.  B  A. y  e.  B  ( x  .+  y )  =  ( y  .+  x ) )
5 rsp2 2775 . . . . 5  |-  ( A. x  e.  B  A. y  e.  B  (
x  .+  y )  =  ( y  .+  x )  ->  (
( x  e.  B  /\  y  e.  B
)  ->  ( x  .+  y )  =  ( y  .+  x ) ) )
65imp 427 . . . 4  |-  ( ( A. x  e.  B  A. y  e.  B  ( x  .+  y )  =  ( y  .+  x )  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
74, 6sylan 469 . . 3  |-  ( ( G  e. CMnd  /\  (
x  e.  B  /\  y  e.  B )
)  ->  ( x  .+  y )  =  ( y  .+  x ) )
87caovcomg 6405 . 2  |-  ( ( G  e. CMnd  /\  ( X  e.  B  /\  Y  e.  B )
)  ->  ( X  .+  Y )  =  ( Y  .+  X ) )
983impb 1191 1  |-  ( ( G  e. CMnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  =  ( Y  .+  X
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 972    = wceq 1403    e. wcel 1840   A.wral 2751   ` cfv 5523  (class class class)co 6232   Basecbs 14731   +g cplusg 14799   Mndcmnd 16133  CMndccmn 17012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3058  df-dif 3414  df-un 3416  df-in 3418  df-ss 3425  df-nul 3736  df-if 3883  df-sn 3970  df-pr 3972  df-op 3976  df-uni 4189  df-br 4393  df-iota 5487  df-fv 5531  df-ov 6235  df-cmn 17014
This theorem is referenced by:  ablcom  17029  cmn32  17030  cmn4  17031  cmn12  17032  mulgnn0di  17048  ghmcmn  17054  subcmn  17059  cntzcmn  17062  prdscmnd  17081  srgcom  17386  srgbinomlem4  17404  csrgbinom  17407  crngcom  17423  lply1binom  18558  ip2di  18864  chfacfscmulgsum  19543  chfacfpmmulgsum  19547  cpmadugsumlemF  19559  omndadd2d  28031  ofldchr  28138
  Copyright terms: Public domain W3C validator