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

Metamath Proof Explorer

Theorem lsmelvalmi

Description: Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmelvalm.m ⊢ − = ( -g ‘ 𝐺 )
lsmelvalm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
lsmelvalm.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmelvalm.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
lsmelvalmi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑇 )
lsmelvalmi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion lsmelvalmi ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lsmelvalm.m ⊢ − = ( -g ‘ 𝐺 )
2 lsmelvalm.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 lsmelvalm.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
4 lsmelvalm.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
5 lsmelvalmi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑇 )
6 lsmelvalmi.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
7 eqidd ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) )
8 rspceov ⊢ ( ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ∧ ( 𝑋 − 𝑌 ) = ( 𝑋 − 𝑌 ) ) → ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 ( 𝑋 − 𝑌 ) = ( 𝑥 − 𝑦 ) )
9 5 6 7 8 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 ( 𝑋 − 𝑌 ) = ( 𝑥 − 𝑦 ) )
10 1 2 3 4 lsmelvalm ⊢ ( 𝜑 → ( ( 𝑋 − 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ 𝑈 ( 𝑋 − 𝑌 ) = ( 𝑥 − 𝑦 ) ) )
11 9 10 mpbird ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )