Theorem lsmelvalx

Description: Subspace sum membership (for a group or vector space). Extended domain version of lsmelval . (Contributed by NM, 28-Jan-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	lsmelvalx	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to \left(X\in \left(T\underset{\dot{}}{\oplus }U\right)\leftrightarrow \exists y\in T\exists z\in UX=y\underset{\dot{}}{+}z\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	1 2 3	lsmvalx	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to T\underset{\dot{}}{\oplus }U=\mathrm{ran}\left(y\in T,z\in U⟼y\underset{\dot{}}{+}z\right)$$
5	4	eleq2d	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to \left(X\in \left(T\underset{\dot{}}{\oplus }U\right)\leftrightarrow X\in \mathrm{ran}\left(y\in T,z\in U⟼y\underset{\dot{}}{+}z\right)\right)$$
6		eqid	$$⊢\left(y\in T,z\in U⟼y\underset{\dot{}}{+}z\right)=\left(y\in T,z\in U⟼y\underset{\dot{}}{+}z\right)$$
7		ovex	$$⊢y\underset{\dot{}}{+}z\in \mathrm{V}$$
8	6 7	elrnmpo	$$⊢X\in \mathrm{ran}\left(y\in T,z\in U⟼y\underset{\dot{}}{+}z\right)\leftrightarrow \exists y\in T\exists z\in UX=y\underset{\dot{}}{+}z$$
9	5 8	syl6bb	$$⊢\left(G\in V\wedge T\subseteq B\wedge U\subseteq B\right)\to \left(X\in \left(T\underset{\dot{}}{\oplus }U\right)\leftrightarrow \exists y\in T\exists z\in UX=y\underset{\dot{}}{+}z\right)$$