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 = {Base}_{G}$
	elgrplsmsn.2	$⊢ \underset{˙}{+} = +_{G}$
	elgrplsmsn.3	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	elgrplsmsn.4	$⊢ φ \to G \in V$
	elgrplsmsn.5	$⊢ φ \to A \subseteq B$
	elgrplsmsn.6	$⊢ φ \to X \in B$
Assertion	elgrplsmsn	$⊢ φ \to (Z \in (A \underset{˙}{\oplus} \{X\}) \leftrightarrow \exists x \in A Z = x \underset{˙}{+} X)$

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

Metamath Proof Explorer