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	⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )