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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	elgrplsmsn.2	⊢ + = ( +g ‘ 𝐺 )
	elgrplsmsn.3	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	elgrplsmsn.4	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	elgrplsmsn.5	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	elgrplsmsn.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	elgrplsmsn	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑍 = ( 𝑥 + 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elgrplsmsn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		elgrplsmsn.2	⊢ + = ( +g ‘ 𝐺 )
3		elgrplsmsn.3	⊢ ⊕ = ( LSSum ‘ 𝐺 )
4		elgrplsmsn.4	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		elgrplsmsn.5	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
6		elgrplsmsn.6	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7	6	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 )
8	1 2 3	lsmelvalx	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ∧ { 𝑋 } ⊆ 𝐵 ) → ( 𝑍 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑋 } 𝑍 = ( 𝑥 + 𝑦 ) ) )
9	4 5 7 8	syl3anc	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑋 } 𝑍 = ( 𝑥 + 𝑦 ) ) )
10		oveq2	⊢ ( 𝑦 = 𝑋 → ( 𝑥 + 𝑦 ) = ( 𝑥 + 𝑋 ) )
11	10	eqeq2d	⊢ ( 𝑦 = 𝑋 → ( 𝑍 = ( 𝑥 + 𝑦 ) ↔ 𝑍 = ( 𝑥 + 𝑋 ) ) )
12	11	rexsng	⊢ ( 𝑋 ∈ 𝐵 → ( ∃ 𝑦 ∈ { 𝑋 } 𝑍 = ( 𝑥 + 𝑦 ) ↔ 𝑍 = ( 𝑥 + 𝑋 ) ) )
13	6 12	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ { 𝑋 } 𝑍 = ( 𝑥 + 𝑦 ) ↔ 𝑍 = ( 𝑥 + 𝑋 ) ) )
14	13	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑋 } 𝑍 = ( 𝑥 + 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑍 = ( 𝑥 + 𝑋 ) ) )
15	9 14	bitrd	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑍 = ( 𝑥 + 𝑋 ) ) )