cmncom

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

	Ref	Expression
Hypotheses	ablcom.b	$⊢ B = {Base}_{G}$
	ablcom.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	cmncom	$⊢ (G \in CMnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

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

Metamath Proof Explorer