Theorem grpidssd

Description: If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then both groups have the same identity element. (Contributed by AV, 15-Mar-2019)

	Ref	Expression
Hypotheses	grpidssd.m	$$⊢\phi \to M\in \mathrm{Grp}$$
	grpidssd.s	$$⊢\phi \to S\in \mathrm{Grp}$$
	grpidssd.b	$$⊢B={\mathrm{Base}}_S$$
	grpidssd.c	$$⊢\phi \to B\subseteq {\mathrm{Base}}_M$$
	grpidssd.o	$$⊢\phi \to \forall x\in B\forall y\in Bx{+}_{M}y=x{+}_{S}y$$
Assertion	grpidssd	$$⊢\phi \to 0_M=0_S$$

Proof

Step	Hyp	Ref	Expression
1		grpidssd.m	$$⊢\phi \to M\in \mathrm{Grp}$$
2		grpidssd.s	$$⊢\phi \to S\in \mathrm{Grp}$$
3		grpidssd.b	$$⊢B={\mathrm{Base}}_S$$
4		grpidssd.c	$$⊢\phi \to B\subseteq {\mathrm{Base}}_M$$
5		grpidssd.o	$$⊢\phi \to \forall x\in B\forall y\in Bx{+}_{M}y=x{+}_{S}y$$
6		eqid	$$⊢0_S=0_S$$
7	3 6	grpidcl	$$⊢S\in \mathrm{Grp}\to 0_S\in B$$
8	2 7	syl	$$⊢\phi \to 0_S\in B$$
9		oveq1	$$⊢x=0_S\to x{+}_{M}y=0_S{+}_{M}y$$
10		oveq1	$$⊢x=0_S\to x{+}_{S}y=0_S{+}_{S}y$$
11	9 10	eqeq12d	$$⊢x=0_S\to \left(x{+}_{M}y=x{+}_{S}y\leftrightarrow 0_S{+}_{M}y=0_S{+}_{S}y\right)$$
12		oveq2	$$⊢y=0_S\to 0_S{+}_{M}y=0_S{+}_M{0}_S$$
13		oveq2	$$⊢y=0_S\to 0_S{+}_{S}y=0_S{+}_S{0}_S$$
14	12 13	eqeq12d	$$⊢y=0_S\to \left(0_S{+}_{M}y=0_S{+}_{S}y\leftrightarrow 0_S{+}_M{0}_S=0_S{+}_S{0}_S\right)$$
15	11 14	rspc2va	$$⊢\left(\left(0_S\in B\wedge 0_S\in B\right)\wedge \forall x\in B\forall y\in Bx{+}_{M}y=x{+}_{S}y\right)\to 0_S{+}_M{0}_S=0_S{+}_S{0}_S$$
16	8 8 5 15	syl21anc	$$⊢\phi \to 0_S{+}_M{0}_S=0_S{+}_S{0}_S$$
17		eqid	$$⊢{+}_S={+}_S$$
18	3 17 6	grplid	$$⊢\left(S\in \mathrm{Grp}\wedge 0_S\in B\right)\to 0_S{+}_S{0}_S=0_S$$
19	2 7 18	syl2anc2	$$⊢\phi \to 0_S{+}_S{0}_S=0_S$$
20	16 19	eqtrd	$$⊢\phi \to 0_S{+}_M{0}_S=0_S$$
21	4 8	sseldd	$$⊢\phi \to 0_S\in {\mathrm{Base}}_M$$
22		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
23		eqid	$$⊢{+}_M={+}_M$$
24		eqid	$$⊢0_M=0_M$$
25	22 23 24	grpidlcan	$$⊢\left(M\in \mathrm{Grp}\wedge 0_S\in {\mathrm{Base}}_M\wedge 0_S\in {\mathrm{Base}}_M\right)\to \left(0_S{+}_M{0}_S=0_S\leftrightarrow 0_S=0_M\right)$$
26	1 21 21 25	syl3anc	$$⊢\phi \to \left(0_S{+}_M{0}_S=0_S\leftrightarrow 0_S=0_M\right)$$
27	20 26	mpbid	$$⊢\phi \to 0_S=0_M$$
28	27	eqcomd	$$⊢\phi \to 0_M=0_S$$