Theorem cmncom

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

	Ref	Expression
Hypotheses	ablcom.b	$$⊢B={\mathrm{Base}}_G$$
	ablcom.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	cmncom	$$⊢\left(G\in \mathrm{CMnd}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		ablcom.b	$$⊢B={\mathrm{Base}}_G$$
2		ablcom.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	iscmn	$$⊢G\in \mathrm{CMnd}\leftrightarrow \left(G\in \mathrm{Mnd}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
4	3	simprbi	$$⊢G\in \mathrm{CMnd}\to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
5		rsp2	$$⊢\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\to \left(\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
6	5	imp	$$⊢\left(\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
7	4 6	sylan	$$⊢\left(G\in \mathrm{CMnd}\wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
8	7	caovcomg	$$⊢\left(G\in \mathrm{CMnd}\wedge \left(X\in B\wedge Y\in B\right)\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
9	8	3impb	$$⊢\left(G\in \mathrm{CMnd}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$