Theorem ablprop

Description: If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013)

	Ref	Expression
Hypotheses	ablprop.b	|- ( Base ` K ) = ( Base ` L )
	ablprop.p	|- ( +g ` K ) = ( +g ` L )
Assertion	ablprop	|- ( K e. Abel <-> L e. Abel )

Proof

Step	Hyp	Ref	Expression
1		ablprop.b	|- ( Base ` K ) = ( Base ` L )
2		ablprop.p	|- ( +g ` K ) = ( +g ` L )
3		eqidd	|- ( T. -> ( Base ` K ) = ( Base ` K ) )
4	1	a1i	|- ( T. -> ( Base ` K ) = ( Base ` L ) )
5	2	oveqi	|- ( x ( +g ` K ) y ) = ( x ( +g ` L ) y )
6	5	a1i	|- ( ( T. /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
7	3 4 6	ablpropd	|- ( T. -> ( K e. Abel <-> L e. Abel ) )
8	7	mptru	|- ( K e. Abel <-> L e. Abel )