This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑍 = ( 𝑥 + 𝑋 ) ) )