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	$$⊢\underset{\dot{}}{-}={-}_G$$
	lsmelvalm.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	lsmelvalm.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	lsmelvalm.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	lsmelvalmi.x	$$⊢\phi \to X\in T$$
	lsmelvalmi.y	$$⊢\phi \to Y\in U$$
Assertion	lsmelvalmi	$$⊢\phi \to X\underset{\dot{}}{-}Y\in \left(T\underset{\dot{}}{\oplus }U\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmelvalm.m	$$⊢\underset{\dot{}}{-}={-}_G$$
2		lsmelvalm.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
3		lsmelvalm.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
4		lsmelvalm.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
5		lsmelvalmi.x	$$⊢\phi \to X\in T$$
6		lsmelvalmi.y	$$⊢\phi \to Y\in U$$
7		eqidd	$$⊢\phi \to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{-}Y$$
8		rspceov	$$⊢\left(X\in T\wedge Y\in U\wedge X\underset{\dot{}}{-}Y=X\underset{\dot{}}{-}Y\right)\to \exists x\in T\exists y\in UX\underset{\dot{}}{-}Y=x\underset{\dot{}}{-}y$$
9	5 6 7 8	syl3anc	$$⊢\phi \to \exists x\in T\exists y\in UX\underset{\dot{}}{-}Y=x\underset{\dot{}}{-}y$$
10	1 2 3 4	lsmelvalm	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\in \left(T\underset{\dot{}}{\oplus }U\right)\leftrightarrow \exists x\in T\exists y\in UX\underset{\dot{}}{-}Y=x\underset{\dot{}}{-}y\right)$$
11	9 10	mpbird	$$⊢\phi \to X\underset{\dot{}}{-}Y\in \left(T\underset{\dot{}}{\oplus }U\right)$$