This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ablcom

Description: An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011)

	Ref	Expression
Hypotheses	ablcom.b	$⊢ B = {Base}_{G}$
	ablcom.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	ablcom	$⊢ (G \in Abel \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		ablcmn	$⊢ G \in Abel \to G \in CMnd$
4	1 2	cmncom	$⊢ (G \in CMnd \land X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
5	3 4	syl3an1	$⊢ (G \in Abel \land X \in B \land Y \in B) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$