Theorem mndprop

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

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

Proof

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