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	3	grpmndd	$$⊢\phi \to G\in \mathrm{Mnd}$$
6	1 2 5 4	iscmnd	$$⊢\phi \to G\in \mathrm{CMnd}$$
7		isabl	$$⊢G\in \mathrm{Abel}\leftrightarrow \left(G\in \mathrm{Grp}\wedge G\in \mathrm{CMnd}\right)$$
8	3 6 7	sylanbrc	$$⊢\phi \to G\in \mathrm{Abel}$$