Theorem isabld

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

	Ref	Expression
Hypotheses	isabld.b	|- ( ph -> B = ( Base ` G ) )
	isabld.p	|- ( ph -> .+ = ( +g ` G ) )
	isabld.g	|- ( ph -> G e. Grp )
	isabld.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )
Assertion	isabld	|- ( ph -> G e. Abel )

Proof

Step	Hyp	Ref	Expression
1		isabld.b	|- ( ph -> B = ( Base ` G ) )
2		isabld.p	|- ( ph -> .+ = ( +g ` G ) )
3		isabld.g	|- ( ph -> G e. Grp )
4		isabld.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )
5	3	grpmndd	|- ( ph -> G e. Mnd )
6	1 2 5 4	iscmnd	|- ( ph -> G e. CMnd )
7		isabl	|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
8	3 6 7	sylanbrc	|- ( ph -> G e. Abel )