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

Theorem cmncom 19747
Description: A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.)
Hypotheses
Ref Expression
ablcom.b 𝐵 = (Base‘𝐺)
ablcom.p + = (+g𝐺)
Assertion
Ref Expression
cmncom ((𝐺 ∈ CMnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))

Proof of Theorem cmncom
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ablcom.b . . . . . 6 𝐵 = (Base‘𝐺)
2 ablcom.p . . . . . 6 + = (+g𝐺)
31, 2iscmn 19738 . . . . 5 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
43simprbi 496 . . . 4 (𝐺 ∈ CMnd → ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))
5 rsp2 3270 . . . . 5 (∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) → ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)))
65imp 406 . . . 4 ((∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
74, 6sylan 579 . . 3 ((𝐺 ∈ CMnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
87caovcomg 7611 . 2 ((𝐺 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵)) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
983impb 1113 1 ((𝐺 ∈ CMnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1534  wcel 2099  wral 3057  cfv 6543  (class class class)co 7415  Basecbs 17174  +gcplusg 17227  Mndcmnd 18688  CMndccmn 19729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418  df-cmn 19731
This theorem is referenced by:  ablcom  19748  cmn32  19749  cmn4  19750  cmn12  19751  cmnbascntr  19754  rinvmod  19755  mulgnn0di  19774  ghmcmn  19780  subcmn  19786  cntzcmn  19789  prdscmnd  19810  srgcom  20140  srgbinomlem4  20163  csrgbinom  20166  crngcom  20185  ip2di  21567  lply1binom  22223  chfacfscmulgsum  22756  chfacfpmmulgsum  22760  cpmadugsumlemF  22772  cmn246135  32748  cmn145236  32749  omndadd2d  32783  rlocaddval  32977  ofldchr  33024  elrspunsn  33140  primrootsunit1  41562  aks6d1c5lem3  41603
  Copyright terms: Public domain W3C validator