Theorem grppropd

Description: If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	grppropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
	grppropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
	grppropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
Assertion	grppropd	$$⊢\phi \to \left(K\in \mathrm{Grp}\leftrightarrow L\in \mathrm{Grp}\right)$$

Proof

Step	Hyp	Ref	Expression
1		grppropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		grppropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		grppropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4	1 2 3	mndpropd	$$⊢\phi \to \left(K\in \mathrm{Mnd}\leftrightarrow L\in \mathrm{Mnd}\right)$$
5	1 2 3	grpidpropd	$$⊢\phi \to 0_K=0_L$$
6	5	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to 0_K=0_L$$
7	3 6	eqeq12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x{+}_{K}y=0_K\leftrightarrow x{+}_{L}y=0_L\right)$$
8	7	anass1rs	$$⊢\left(\left(\phi \wedge y\in B\right)\wedge x\in B\right)\to \left(x{+}_{K}y=0_K\leftrightarrow x{+}_{L}y=0_L\right)$$
9	8	rexbidva	$$⊢\left(\phi \wedge y\in B\right)\to \left(\exists x\in Bx{+}_{K}y=0_K\leftrightarrow \exists x\in Bx{+}_{L}y=0_L\right)$$
10	9	ralbidva	$$⊢\phi \to \left(\forall y\in B\exists x\in Bx{+}_{K}y=0_K\leftrightarrow \forall y\in B\exists x\in Bx{+}_{L}y=0_L\right)$$
11	1	rexeqdv	$$⊢\phi \to \left(\exists x\in Bx{+}_{K}y=0_K\leftrightarrow \exists x\in {\mathrm{Base}}_{K}x{+}_{K}y=0_K\right)$$
12	1 11	raleqbidv	$$⊢\phi \to \left(\forall y\in B\exists x\in Bx{+}_{K}y=0_K\leftrightarrow \forall y\in {\mathrm{Base}}_K\exists x\in {\mathrm{Base}}_{K}x{+}_{K}y=0_K\right)$$
13	2	rexeqdv	$$⊢\phi \to \left(\exists x\in Bx{+}_{L}y=0_L\leftrightarrow \exists x\in {\mathrm{Base}}_{L}x{+}_{L}y=0_L\right)$$
14	2 13	raleqbidv	$$⊢\phi \to \left(\forall y\in B\exists x\in Bx{+}_{L}y=0_L\leftrightarrow \forall y\in {\mathrm{Base}}_L\exists x\in {\mathrm{Base}}_{L}x{+}_{L}y=0_L\right)$$
15	10 12 14	3bitr3d	$$⊢\phi \to \left(\forall y\in {\mathrm{Base}}_K\exists x\in {\mathrm{Base}}_{K}x{+}_{K}y=0_K\leftrightarrow \forall y\in {\mathrm{Base}}_L\exists x\in {\mathrm{Base}}_{L}x{+}_{L}y=0_L\right)$$
16	4 15	anbi12d	$$⊢\phi \to \left(\left(K\in \mathrm{Mnd}\wedge \forall y\in {\mathrm{Base}}_K\exists x\in {\mathrm{Base}}_{K}x{+}_{K}y=0_K\right)\leftrightarrow \left(L\in \mathrm{Mnd}\wedge \forall y\in {\mathrm{Base}}_L\exists x\in {\mathrm{Base}}_{L}x{+}_{L}y=0_L\right)\right)$$
17		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
18		eqid	$$⊢{+}_K={+}_K$$
19		eqid	$$⊢0_K=0_K$$
20	17 18 19	isgrp	$$⊢K\in \mathrm{Grp}\leftrightarrow \left(K\in \mathrm{Mnd}\wedge \forall y\in {\mathrm{Base}}_K\exists x\in {\mathrm{Base}}_{K}x{+}_{K}y=0_K\right)$$
21		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
22		eqid	$$⊢{+}_L={+}_L$$
23		eqid	$$⊢0_L=0_L$$
24	21 22 23	isgrp	$$⊢L\in \mathrm{Grp}\leftrightarrow \left(L\in \mathrm{Mnd}\wedge \forall y\in {\mathrm{Base}}_L\exists x\in {\mathrm{Base}}_{L}x{+}_{L}y=0_L\right)$$
25	16 20 24	3bitr4g	$$⊢\phi \to \left(K\in \mathrm{Grp}\leftrightarrow L\in \mathrm{Grp}\right)$$