Theorem cmncom

Description: A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	ablcom.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablcom.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	cmncom	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

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