Theorem idressidex

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$$
Assertion	idressidex	$$⊢\phi \to \exists e\in A\forall x\in A\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		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
9	1 2 3 4 5 6 7 8	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)$$
10	5 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_S$$
11		id	$$⊢A={\mathrm{Base}}_S\to A={\mathrm{Base}}_S$$
12		raleq	$$⊢A={\mathrm{Base}}_S\to \left(\forall x\in A\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_S\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)\right)$$
13	11 12	rexeqbidv	$$⊢A={\mathrm{Base}}_S\to \left(\exists e\in A\forall x\in A\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}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)$$
14	6 10 13	3syl	$$⊢\phi \to \left(\exists e\in A\forall x\in A\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}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)$$
15	9 14	mpbird	$$⊢\phi \to \exists e\in A\forall x\in A\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$