Theorem cmncom 19711

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.

Step	Hyp	Ref	Expression
1		ablcom.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
2		ablcom.p	. . . . . 6 ⊢ + = (+g‘𝐺)
3	1, 2	iscmn 19702	. . . . 5 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
4	3	simprbi 496	. . . 4 ⊢ (𝐺 ∈ CMnd → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))
5		rsp2 3249	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)))
6	5	imp 406	. . . 4 ⊢ ((∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
7	4, 6	sylan 580	. . 3 ⊢ ((𝐺 ∈ CMnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
8	7	caovcomg 7541	. 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
9	8	3impb 1114	1 ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17120  +_gcplusg 17161  Mndcmnd 18642  CMndccmn 19693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-cmn 19695

This theorem is referenced by:  ablcom  19712  cmn32  19713  cmn4  19714  cmn12  19715  cmnbascntr  19718  rinvmod  19719  mulgnn0di  19738  ghmcmn  19744  subcmn  19750  cntzcmn  19753  prdscmnd  19774  omndadd2d  20043  srgcom  20125  srgbinomlem4  20148  csrgbinom  20151  crngcom  20170  ofldchr  21514  ip2di  21579  lply1binom  22226  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  cpmadugsumlemF  22792  cmn246135  33012  cmn145236  33013  gsumwun  33043  rlocaddval  33233  elrspunsn  33392  evl1deg2  33538  evl1deg3  33539  primrootsunit1  42136  aks6d1c5lem3  42176