Theorem grpidpropd

Description: If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		grpidpropd.1	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		grpidpropd.2	$$⊢\phi \to B={\mathrm{Base}}_L$$
3		grpidpropd.3	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{K}y=x{+}_{L}y$$
4	3	eqeq1d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(x{+}_{K}y=y\leftrightarrow x{+}_{L}y=y\right)$$
5	3	oveqrspc2v	$$⊢\left(\phi \wedge \left(z\in B\wedge w\in B\right)\right)\to z{+}_{K}w=z{+}_{L}w$$
6	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(y\in B\wedge x\in B\right)\right)\to y{+}_{K}x=y{+}_{L}x$$
7	6	ancom2s	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y{+}_{K}x=y{+}_{L}x$$
8	7	eqeq1d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(y{+}_{K}x=y\leftrightarrow y{+}_{L}x=y\right)$$
9	4 8	anbi12d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\leftrightarrow \left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)$$
10	9	anassrs	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in B\right)\to \left(\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\leftrightarrow \left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)$$
11	10	ralbidva	$$⊢\left(\phi \wedge x\in B\right)\to \left(\forall y\in B\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\leftrightarrow \forall y\in B\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)$$
12	11	pm5.32da	$$⊢\phi \to \left(\left(x\in B\wedge \forall y\in B\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\leftrightarrow \left(x\in B\wedge \forall y\in B\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\right)$$
13	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_K\right)$$
14	1	raleqdv	$$⊢\phi \to \left(\forall y\in B\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\leftrightarrow \forall y\in {\mathrm{Base}}_K\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)$$
15	13 14	anbi12d	$$⊢\phi \to \left(\left(x\in B\wedge \forall y\in B\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\leftrightarrow \left(x\in {\mathrm{Base}}_K\wedge \forall y\in {\mathrm{Base}}_K\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\right)$$
16	2	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_L\right)$$
17	2	raleqdv	$$⊢\phi \to \left(\forall y\in B\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\leftrightarrow \forall y\in {\mathrm{Base}}_L\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)$$
18	16 17	anbi12d	$$⊢\phi \to \left(\left(x\in B\wedge \forall y\in B\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\leftrightarrow \left(x\in {\mathrm{Base}}_L\wedge \forall y\in {\mathrm{Base}}_L\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\right)$$
19	12 15 18	3bitr3d	$$⊢\phi \to \left(\left(x\in {\mathrm{Base}}_K\wedge \forall y\in {\mathrm{Base}}_K\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\leftrightarrow \left(x\in {\mathrm{Base}}_L\wedge \forall y\in {\mathrm{Base}}_L\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\right)$$
20	19	iotabidv	$$⊢\phi \to \left(\iota x|\left(x\in {\mathrm{Base}}_K\wedge \forall y\in {\mathrm{Base}}_K\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\right)=\left(\iota x|\left(x\in {\mathrm{Base}}_L\wedge \forall y\in {\mathrm{Base}}_L\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\right)$$
21		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
22		eqid	$$⊢{+}_K={+}_K$$
23		eqid	$$⊢0_K=0_K$$
24	21 22 23	grpidval	$$⊢0_K=\left(\iota x|\left(x\in {\mathrm{Base}}_K\wedge \forall y\in {\mathrm{Base}}_K\left(x{+}_{K}y=y\wedge y{+}_{K}x=y\right)\right)\right)$$
25		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
26		eqid	$$⊢{+}_L={+}_L$$
27		eqid	$$⊢0_L=0_L$$
28	25 26 27	grpidval	$$⊢0_L=\left(\iota x|\left(x\in {\mathrm{Base}}_L\wedge \forall y\in {\mathrm{Base}}_L\left(x{+}_{L}y=y\wedge y{+}_{L}x=y\right)\right)\right)$$
29	20 24 28	3eqtr4g	$$⊢\phi \to 0_K=0_L$$