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

Theorem ablcom 15412
Description: An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
Hypotheses
Ref Expression
ablcom.b  |-  B  =  ( Base `  G
)
ablcom.p  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
ablcom  |-  ( ( G  e.  Abel  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  =  ( Y  .+  X
) )

Proof of Theorem ablcom
StepHypRef Expression
1 ablcmn 15401 . 2  |-  ( G  e.  Abel  ->  G  e. CMnd
)
2 ablcom.b . . 3  |-  B  =  ( Base `  G
)
3 ablcom.p . . 3  |-  .+  =  ( +g  `  G )
42, 3cmncom 15411 . 2  |-  ( ( G  e. CMnd  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  =  ( Y  .+  X
) )
51, 4syl3an1 1217 1  |-  ( ( G  e.  Abel  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .+  Y )  =  ( Y  .+  X
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1652    e. wcel 1725   ` cfv 5440  (class class class)co 6067   Basecbs 13452   +g cplusg 13512  CMndccmn 15395   Abelcabel 15396
This theorem is referenced by:  ablinvadd  15417  ablsub2inv  15418  ablsubadd  15419  abladdsub  15422  ablpncan3  15424  ablsub32  15429  eqgabl  15437  subgabl  15438  ablnsg  15445  lsmcomx  15454  divsabl  15463  frgpnabl  15469  ngplcan  18640  r1pid  20065  cnaddcom  29500  toycom  29501  lflsub  29596  lfladdcom  29601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070  df-cmn 15397  df-abl 15398
  Copyright terms: Public domain W3C validator