Metamath Proof Explorer


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 )