Theorem 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={\mathrm{Base}}_G$$
	iscmn.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	isabl2	$$⊢G\in \mathrm{Abel}\leftrightarrow \left(G\in \mathrm{Grp}\wedge \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$

Proof

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