Theorem cmncom 19784

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 19775	. . . . 5 ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
4	3	simprbi 496	. . . 4 ⊢ (𝐺 ∈ CMnd → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))
5		rsp2 3263	. . . . 5 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)))
6	5	imp 406	. . . 4 ⊢ ((∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
7	4, 6	sylan 580	. . 3 ⊢ ((𝐺 ∈ CMnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))
8	7	caovcomg 7607	. 2 ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
9	8	3impb 1114	1 ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  Mndcmnd 18717  CMndccmn 19766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-cmn 19768

This theorem is referenced by:  ablcom  19785  cmn32  19786  cmn4  19787  cmn12  19788  cmnbascntr  19791  rinvmod  19792  mulgnn0di  19811  ghmcmn  19817  subcmn  19823  cntzcmn  19826  prdscmnd  19847  srgcom  20171  srgbinomlem4  20194  csrgbinom  20197  crngcom  20216  ip2di  21606  lply1binom  22253  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  cpmadugsumlemF  22819  cmn246135  33033  cmn145236  33034  gsumwun  33064  omndadd2d  33081  rlocaddval  33268  ofldchr  33341  elrspunsn  33449  evl1deg2  33595  evl1deg3  33596  primrootsunit1  42115  aks6d1c5lem3  42155