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 ‘ 𝐾 ) = ( Base ‘ 𝐿 )
	mndprop.p	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 )
Assertion	mndprop	⊢ ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		mndprop.b	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 )
2		mndprop.p	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐿 )
3		eqidd	⊢ ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
4	1	a1i	⊢ ( ⊤ → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐿 ) )
5	2	oveqi	⊢ ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 )
6	5	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
7	3 4 6	mndpropd	⊢ ( ⊤ → ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd ) )
8	7	mptru	⊢ ( 𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd )