Theorem isabli

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

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

Proof

Step	Hyp	Ref	Expression
1		isabli.g	|- G e. Grp
2		isabli.b	|- B = ( Base ` G )
3		isabli.p	|- .+ = ( +g ` G )
4		isabli.c	|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )
5	4	rgen2	|- A. x e. B A. y e. B ( x .+ y ) = ( y .+ x )
6	2 3	isabl2	|- ( G e. Abel <-> ( G e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
7	1 5 6	mpbir2an	|- G e. Abel