isabl2

Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	iscmn.b	$⊢ B = {Base}_{G}$
	iscmn.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	isabl2	$⊢ G \in Abel \leftrightarrow (G \in Grp \land \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$

Step	Hyp	Ref	Expression
1		iscmn.b	$⊢ B = {Base}_{G}$
2		iscmn.p	$⊢ \underset{˙}{+} = +_{G}$
3		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
4		grpmnd	$⊢ G \in Grp \to G \in Mnd$
5	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)$
6	5	baib	$⊢ G \in Mnd \to (G \in CMnd \leftrightarrow \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$
7	4 6	syl	$⊢ G \in Grp \to (G \in CMnd \leftrightarrow \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$
8	7	pm5.32i	$⊢ (G \in Grp \land G \in CMnd) \leftrightarrow (G \in Grp \land \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$
9	3 8	bitri	$⊢ G \in Abel \leftrightarrow (G \in Grp \land \forall x \in B \forall y \in B x \underset{˙}{+} y = y \underset{˙}{+} x)$

Metamath Proof Explorer