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

Theorem cmncom 18032
 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 18023 . . . . 5 (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
43simprbi 479 . . . 4 (𝐺 ∈ CMnd → ∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))
5 rsp2 2920 . . . . 5 (∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) → ((𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)))
65imp 444 . . . 4 ((∀𝑥𝐵𝑦𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
74, 6sylan 487 . . 3 ((𝐺 ∈ CMnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
87caovcomg 6727 . 2 ((𝐺 ∈ CMnd ∧ (𝑋𝐵𝑌𝐵)) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
983impb 1252 1 ((𝐺 ∈ CMnd ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +gcplusg 15768  Mndcmnd 17117  CMndccmn 18016 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-cmn 18018 This theorem is referenced by:  ablcom  18033  cmn32  18034  cmn4  18035  cmn12  18036  mulgnn0di  18054  ghmcmn  18060  subcmn  18065  cntzcmn  18068  prdscmnd  18087  srgcom  18348  srgbinomlem4  18366  csrgbinom  18369  crngcom  18385  lply1binom  19497  ip2di  19805  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cpmadugsumlemF  20500  omndadd2d  29039  ofldchr  29145
 Copyright terms: Public domain W3C validator