Theorem lsmelvalix

Description: Subspace sum membership (for a group or vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmfval.v	$$⊢B={\mathrm{Base}}_G$$
	lsmfval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	lsmfval.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
Assertion	lsmelvalix	$$⊢\left(\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\wedge \left(X\in T\wedge Y\in U\right)\right)\to X\underset{\dot{}}{+}Y\in \left(T\underset{\dot{}}{\oplus }U\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsmfval.v	$$⊢B={\mathrm{Base}}_G$$
2		lsmfval.a	$$⊢\underset{\dot{}}{+}={+}_G$$
3		lsmfval.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
4		eqid	$$⊢X\underset{\dot{}}{+}Y=X\underset{\dot{}}{+}Y$$
5		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$$
6	4 5	mp3an3	$$⊢\left(X\in T\wedge Y\in U\right)\to \exists x\in T\exists y\in UX\underset{\dot{}}{+}Y=x\underset{\dot{}}{+}y$$
7	1 2 3	lsmelvalx	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\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)$$
8	7	biimpar	$$⊢\left(\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\wedge \exists x\in T\exists y\in UX\underset{\dot{}}{+}Y=x\underset{\dot{}}{+}y\right)\to X\underset{\dot{}}{+}Y\in \left(T\underset{\dot{}}{\oplus }U\right)$$
9	6 8	sylan2	$$⊢\left(\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\wedge \left(X\in T\wedge Y\in U\right)\right)\to X\underset{\dot{}}{+}Y\in \left(T\underset{\dot{}}{\oplus }U\right)$$