Theorem isabli

Description: Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011)

	Ref	Expression
Hypotheses	isabli.g	$$⊢G\in \mathrm{Grp}$$
	isabli.b	$$⊢B={\mathrm{Base}}_G$$
	isabli.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	isabli.c	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
Assertion	isabli	$$⊢G\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		isabli.g	$$⊢G\in \mathrm{Grp}$$
2		isabli.b	$$⊢B={\mathrm{Base}}_G$$
3		isabli.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		isabli.c	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
5	4	rgen2	$$⊢\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
6	2 3	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)$$
7	1 5 6	mpbir2an	$$⊢G\in \mathrm{Abel}$$