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

Theorem ablcom 19667
Description: An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.)
Hypotheses
Ref Expression
ablcom.b 𝐵 = (Base‘𝐺)
ablcom.p + = (+g𝐺)
Assertion
Ref Expression
ablcom ((𝐺 ∈ Abel ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))

Proof of Theorem ablcom
StepHypRef Expression
1 ablcmn 19655 . 2 (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
2 ablcom.b . . 3 𝐵 = (Base‘𝐺)
3 ablcom.p . . 3 + = (+g𝐺)
42, 3cmncom 19666 . 2 ((𝐺 ∈ CMnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
51, 4syl3an1 1164 1 ((𝐺 ∈ Abel ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  cfv 6544  (class class class)co 7409  Basecbs 17144  +gcplusg 17197  CMndccmn 19648  Abelcabl 19649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-cmn 19650  df-abl 19651
This theorem is referenced by:  ablinvadd  19675  ablsub2inv  19676  ablsubadd  19677  abladdsub  19680  ablsubaddsub  19682  ablpncan3  19684  ablsub32  19689  ablnnncan  19690  ablsubsub23  19692  eqgabl  19702  subgabl  19704  ablnsg  19715  lsmcomx  19724  qusabl  19733  frgpnabl  19743  imasabl  19744  ngplcan  24120  clmnegsubdi2  24621  clmvsubval2  24626  ncvspi  24673  r1pid  25677  abliso  32197  lindsunlem  32709  cnaddcom  37842  toycom  37843  lflsub  37937  lfladdcom  37942  subrngringnsg  46732
  Copyright terms: Public domain W3C validator