Theorem isabld

Description: Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013)

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

Proof

Step	Hyp	Ref	Expression
1		isabld.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
2		isabld.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
3		isabld.g	$$⊢\phi \to G\in \mathrm{Grp}$$
4		isabld.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
5		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
6	3 5	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
7	1 2 6 4	iscmnd	$$⊢\phi \to G\in \mathrm{CMnd}$$
8		isabl	$$⊢G\in \mathrm{Abel}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{CMnd}\right)$$
9	3 7 8	sylanbrc	$$⊢\phi \to G\in \mathrm{Abel}$$