Theorem idressidex0

Description: The restriction of a structure with an identity element to a subset containing the identity element has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 11-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$$
	idressidex0.c	$$⊢C={\mathrm{Base}}_S$$
Assertion	idressidex0	$$⊢\phi \to \exists e\in C\forall x\in C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$

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		idressidex0.c	$$⊢C={\mathrm{Base}}_S$$
9	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)$$
10	5 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_S$$
11	6 10	syl	$$⊢\phi \to A={\mathrm{Base}}_S$$
12	8 11	eqtr4id	$$⊢\phi \to C=A$$
13	7 12	eleqtrrd	$$⊢\phi \to \underset{\dot{}}{0}\in C$$
14	5 1	ressbasss	$$⊢{\mathrm{Base}}_S\subseteq B$$
15	8 14	eqsstri	$$⊢C\subseteq B$$
16		ssralv	$$⊢C\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 C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
17	15 16	mp1i	$$⊢\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 C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
18	17	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 C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
19	18	adantr	$$⊢\left(\phi \wedge e=\underset{\dot{}}{0}\right)\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 C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
20		oveq1	$$⊢e=\underset{\dot{}}{0}\to e\underset{\dot{}}{+}x=\underset{\dot{}}{0}\underset{\dot{}}{+}x$$
21	20	eqeq1d	$$⊢e=\underset{\dot{}}{0}\to \left(e\underset{\dot{}}{+}x=x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{+}x=x\right)$$
22	21	ovanraleqv	$$⊢e=\underset{\dot{}}{0}\to \left(\forall x\in C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \forall x\in C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
23	22	adantl	$$⊢\left(\phi \wedge e=\underset{\dot{}}{0}\right)\to \left(\forall x\in C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \forall x\in C\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
24	19 23	sylibrd	$$⊢\left(\phi \wedge e=\underset{\dot{}}{0}\right)\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 C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
25	13 24	rspcimedv	$$⊢\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 \exists e\in C\forall x\in C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
26	9 25	mpd	$$⊢\phi \to \exists e\in C\forall x\in C\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$