Theorem ablprop

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

	Ref	Expression
Hypotheses	ablprop.b	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
	ablprop.p	$$⊢{+}_K={+}_L$$
Assertion	ablprop	$$⊢K\in \mathrm{Abel}\leftrightarrow L\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		ablprop.b	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_L$$
2		ablprop.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	ablpropd	$$⊢\top \to \left(K\in \mathrm{Abel}\leftrightarrow L\in \mathrm{Abel}\right)$$
8	7	mptru	$$⊢K\in \mathrm{Abel}\leftrightarrow L\in \mathrm{Abel}$$