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	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
	mndprop.p	$$⊢{+}_K={+}_L$$
Assertion	mndprop	$$⊢K\in \mathrm{Mnd}\leftrightarrow L\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		mndprop.b	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		mndprop.p	$$⊢{+}_K={+}_L$$
3		eqidd	$$⊢\top \to {\mathrm{Base}}_K={\mathrm{Base}}_K$$
4	1	a1i	$$⊢\top \to {\mathrm{Base}}_K={\mathrm{Base}}_L$$
5	2	oveqi	$$⊢x{+}_{K}y=x{+}_{L}y$$
6	5	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_K\wedge y\in {\mathrm{Base}}_K\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
7	3 4 6	mndpropd	$$⊢\top \to \left(K\in \mathrm{Mnd}\leftrightarrow L\in \mathrm{Mnd}\right)$$
8	7	mptru	$$⊢K\in \mathrm{Mnd}\leftrightarrow L\in \mathrm{Mnd}$$