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		grpmnd	|- ( G e. Grp -> G e. Mnd )
6	3 5	syl	|- ( ph -> G e. Mnd )
7	1 2 6 4	iscmnd	|- ( ph -> G e. CMnd )
8		isabl	|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
9	3 7 8	sylanbrc	|- ( ph -> G e. Abel )