Theorem grpprop

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

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

Proof

Step	Hyp	Ref	Expression
1		grpprop.b	|- ( Base ` K ) = ( Base ` L )
2		grpprop.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	grppropd	|- ( T. -> ( K e. Grp <-> L e. Grp ) )
8	7	mptru	|- ( K e. Grp <-> L e. Grp )