Theorem grpprop

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

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

Proof

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