Theorem idressid

Description: The restriction of a structure with an identity element to a subset containing the identity element has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 12-Aug-2026)

	Ref	Expression
Hypotheses	idressidex.b	$$⊢B={\mathrm{Base}}_G$$
	idressidex.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	idressidex.o	$$⊢\underset{\dot{}}{0}=0_G$$
	idressidex.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
	idressidex.s	$$⊢S=G{\upharpoonright }_{𝑠}A$$
	idressidex.a	$$⊢\phi \to A\subseteq B$$
	idressidex.0	$$⊢\phi \to \underset{\dot{}}{0}\in A$$
Assertion	idressid	$$⊢\phi \to 0_S=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		idressidex.b	$$⊢B={\mathrm{Base}}_G$$
2		idressidex.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		idressidex.o	$$⊢\underset{\dot{}}{0}=0_G$$
4		idressidex.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
5		idressidex.s	$$⊢S=G{\upharpoonright }_{𝑠}A$$
6		idressidex.a	$$⊢\phi \to A\subseteq B$$
7		idressidex.0	$$⊢\phi \to \underset{\dot{}}{0}\in A$$
8	5 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_S$$
9	6 8	syl	$$⊢\phi \to A={\mathrm{Base}}_S$$
10	7 9	eleqtrd	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_S$$
11	1 3 2 4	0gisid	$$⊢\phi \to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
12		ssralv	$$⊢A\subseteq B\to \left(\forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\to \forall x\in A\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
13	6 12	syl	$$⊢\phi \to \left(\forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\to \forall x\in A\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
14	1	fvexi	$$⊢B\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to B\in \mathrm{V}$$
16	15 6	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
17	5 2	ressplusg	$$⊢A\in \mathrm{V}\to \underset{\dot{}}{+}={+}_S$$
18	16 17	syl	$$⊢\phi \to \underset{\dot{}}{+}={+}_S$$
19	18	oveqd	$$⊢\phi \to \underset{\dot{}}{0}\underset{\dot{}}{+}x=\underset{\dot{}}{0}{+}_{S}x$$
20	19	eqeq1d	$$⊢\phi \to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}{+}_{S}x=x\right)$$
21	18	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x{+}_S\underset{\dot{}}{0}$$
22	21	eqeq1d	$$⊢\phi \to \left(x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\leftrightarrow x{+}_S\underset{\dot{}}{0}=x\right)$$
23	20 22	anbi12d	$$⊢\phi \to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\leftrightarrow \left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)\right)$$
24	9 23	raleqbidv	$$⊢\phi \to \left(\forall x\in A\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_S\left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)\right)$$
25	13 24	sylibd	$$⊢\phi \to \left(\forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\to \forall x\in {\mathrm{Base}}_S\left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)\right)$$
26	25	adantld	$$⊢\phi \to \left(\left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\to \forall x\in {\mathrm{Base}}_S\left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)\right)$$
27	11 26	mpd	$$⊢\phi \to \forall x\in {\mathrm{Base}}_S\left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)$$
28		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
29		eqid	$$⊢0_S=0_S$$
30		eqid	$$⊢{+}_S={+}_S$$
31	1 2 3 4 5 6 7 28	idressidex0	$$⊢\phi \to \exists e\in {\mathrm{Base}}_S\forall x\in {\mathrm{Base}}_S\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
32	18	eqcomd	$$⊢\phi \to {+}_S=\underset{\dot{}}{+}$$
33	32	oveqd	$$⊢\phi \to e{+}_{S}x=e\underset{\dot{}}{+}x$$
34	33	eqeq1d	$$⊢\phi \to \left(e{+}_{S}x=x\leftrightarrow e\underset{\dot{}}{+}x=x\right)$$
35	32	oveqd	$$⊢\phi \to x{+}_{S}e=x\underset{\dot{}}{+}e$$
36	35	eqeq1d	$$⊢\phi \to \left(x{+}_{S}e=x\leftrightarrow x\underset{\dot{}}{+}e=x\right)$$
37	34 36	anbi12d	$$⊢\phi \to \left(\left(e{+}_{S}x=x\wedge x{+}_{S}e=x\right)\leftrightarrow \left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
38	37	ralbidv	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_S\left(e{+}_{S}x=x\wedge x{+}_{S}e=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_S\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
39	38	rexbidv	$$⊢\phi \to \left(\exists e\in {\mathrm{Base}}_S\forall x\in {\mathrm{Base}}_S\left(e{+}_{S}x=x\wedge x{+}_{S}e=x\right)\leftrightarrow \exists e\in {\mathrm{Base}}_S\forall x\in {\mathrm{Base}}_S\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
40	31 39	mpbird	$$⊢\phi \to \exists e\in {\mathrm{Base}}_S\forall x\in {\mathrm{Base}}_S\left(e{+}_{S}x=x\wedge x{+}_{S}e=x\right)$$
41	28 29 30 40	ismgmid	$$⊢\phi \to \left(\left(\underset{\dot{}}{0}\in {\mathrm{Base}}_S\wedge \forall x\in {\mathrm{Base}}_S\left(\underset{\dot{}}{0}{+}_{S}x=x\wedge x{+}_S\underset{\dot{}}{0}=x\right)\right)\leftrightarrow 0_S=\underset{\dot{}}{0}\right)$$
42	10 27 41	mpbi2and	$$⊢\phi \to 0_S=\underset{\dot{}}{0}$$