Theorem elgrplsmsn

Description: Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024)

	Ref	Expression
Hypotheses	elgrplsmsn.1	$$⊢B={\mathrm{Base}}_G$$
	elgrplsmsn.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	elgrplsmsn.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	elgrplsmsn.4	$$⊢\phi \to G\in V$$
	elgrplsmsn.5	$$⊢\phi \to A\subseteq B$$
	elgrplsmsn.6	$$⊢\phi \to X\in B$$
Assertion	elgrplsmsn	$$⊢\phi \to \left(Z\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists x\in AZ=x\underset{\dot{}}{+}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		elgrplsmsn.1	$$⊢B={\mathrm{Base}}_G$$
2		elgrplsmsn.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		elgrplsmsn.3	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		elgrplsmsn.4	$$⊢\phi \to G\in V$$
5		elgrplsmsn.5	$$⊢\phi \to A\subseteq B$$
6		elgrplsmsn.6	$$⊢\phi \to X\in B$$
7	6	snssd	$$⊢\phi \to \left\{X\right\}\subseteq B$$
8	1 2 3	lsmelvalx	$$⊢\left(G\in V\wedge A\subseteq B\wedge \left\{X\right\}\subseteq B\right)\to \left(Z\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists x\in A\exists y\in \left\{X\right\}Z=x\underset{\dot{}}{+}y\right)$$
9	4 5 7 8	syl3anc	$$⊢\phi \to \left(Z\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists x\in A\exists y\in \left\{X\right\}Z=x\underset{\dot{}}{+}y\right)$$
10		oveq2	$$⊢y=X\to x\underset{\dot{}}{+}y=x\underset{\dot{}}{+}X$$
11	10	eqeq2d	$$⊢y=X\to \left(Z=x\underset{\dot{}}{+}y\leftrightarrow Z=x\underset{\dot{}}{+}X\right)$$
12	11	rexsng	$$⊢X\in B\to \left(\exists y\in \left\{X\right\}Z=x\underset{\dot{}}{+}y\leftrightarrow Z=x\underset{\dot{}}{+}X\right)$$
13	6 12	syl	$$⊢\phi \to \left(\exists y\in \left\{X\right\}Z=x\underset{\dot{}}{+}y\leftrightarrow Z=x\underset{\dot{}}{+}X\right)$$
14	13	rexbidv	$$⊢\phi \to \left(\exists x\in A\exists y\in \left\{X\right\}Z=x\underset{\dot{}}{+}y\leftrightarrow \exists x\in AZ=x\underset{\dot{}}{+}X\right)$$
15	9 14	bitrd	$$⊢\phi \to \left(Z\in \left(A\underset{\dot{}}{\oplus }\left\{X\right\}\right)\leftrightarrow \exists x\in AZ=x\underset{\dot{}}{+}X\right)$$