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 = ( Base ` G )
	elgrplsmsn.2	|- .+ = ( +g ` G )
	elgrplsmsn.3	|- .(+) = ( LSSum ` G )
	elgrplsmsn.4	|- ( ph -> G e. V )
	elgrplsmsn.5	|- ( ph -> A C_ B )
	elgrplsmsn.6	|- ( ph -> X e. B )
Assertion	elgrplsmsn	|- ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A Z = ( x .+ X ) ) )

Proof

Step	Hyp	Ref	Expression
1		elgrplsmsn.1	|- B = ( Base ` G )
2		elgrplsmsn.2	|- .+ = ( +g ` G )
3		elgrplsmsn.3	|- .(+) = ( LSSum ` G )
4		elgrplsmsn.4	|- ( ph -> G e. V )
5		elgrplsmsn.5	|- ( ph -> A C_ B )
6		elgrplsmsn.6	|- ( ph -> X e. B )
7	6	snssd	|- ( ph -> { X } C_ B )
8	1 2 3	lsmelvalx	|- ( ( G e. V /\ A C_ B /\ { X } C_ B ) -> ( Z e. ( A .(+) { X } ) <-> E. x e. A E. y e. { X } Z = ( x .+ y ) ) )
9	4 5 7 8	syl3anc	|- ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A E. y e. { X } Z = ( x .+ y ) ) )
10		oveq2	|- ( y = X -> ( x .+ y ) = ( x .+ X ) )
11	10	eqeq2d	|- ( y = X -> ( Z = ( x .+ y ) <-> Z = ( x .+ X ) ) )
12	11	rexsng	|- ( X e. B -> ( E. y e. { X } Z = ( x .+ y ) <-> Z = ( x .+ X ) ) )
13	6 12	syl	|- ( ph -> ( E. y e. { X } Z = ( x .+ y ) <-> Z = ( x .+ X ) ) )
14	13	rexbidv	|- ( ph -> ( E. x e. A E. y e. { X } Z = ( x .+ y ) <-> E. x e. A Z = ( x .+ X ) ) )
15	9 14	bitrd	|- ( ph -> ( Z e. ( A .(+) { X } ) <-> E. x e. A Z = ( x .+ X ) ) )