Theorem lspprel

Description: Member of the span of a pair of vectors. (Contributed by NM, 10-Apr-2015)

	Ref	Expression
Hypotheses	lsppr.v	$$⊢V={\mathrm{Base}}_W$$
	lsppr.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	lsppr.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lsppr.k	$$⊢K={\mathrm{Base}}_F$$
	lsppr.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lsppr.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsppr.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsppr.x	$$⊢\phi \to X\in V$$
	lsppr.y	$$⊢\phi \to Y\in V$$
Assertion	lspprel	$$⊢\phi \to \left(Z\in N\left(\left\{X,Y\right\}\right)\leftrightarrow \exists k\in K\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsppr.v	$$⊢V={\mathrm{Base}}_W$$
2		lsppr.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lsppr.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lsppr.k	$$⊢K={\mathrm{Base}}_F$$
5		lsppr.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lsppr.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
7		lsppr.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		lsppr.x	$$⊢\phi \to X\in V$$
9		lsppr.y	$$⊢\phi \to Y\in V$$
10	1 2 3 4 5 6 7 8 9	lsppr	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)=\left\{v|\exists k\in K\exists l\in Kv=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right\}$$
11	10	eleq2d	$$⊢\phi \to \left(Z\in N\left(\left\{X,Y\right\}\right)\leftrightarrow Z\in \left\{v|\exists k\in K\exists l\in Kv=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right\}\right)$$
12		id	$$⊢Z=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\to Z=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)$$
13		ovex	$$⊢\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\in \mathrm{V}$$
14	12 13	eqeltrdi	$$⊢Z=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\to Z\in \mathrm{V}$$
15	14	rexlimivw	$$⊢\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\to Z\in \mathrm{V}$$
16	15	rexlimivw	$$⊢\exists k\in K\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\to Z\in \mathrm{V}$$
17		eqeq1	$$⊢v=Z\to \left(v=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\leftrightarrow Z=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right)$$
18	17	2rexbidv	$$⊢v=Z\to \left(\exists k\in K\exists l\in Kv=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\leftrightarrow \exists k\in K\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right)$$
19	16 18	elab3	$$⊢Z\in \left\{v|\exists k\in K\exists l\in Kv=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right\}\leftrightarrow \exists k\in K\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)$$
20	11 19	bitrdi	$$⊢\phi \to \left(Z\in N\left(\left\{X,Y\right\}\right)\leftrightarrow \exists k\in K\exists l\in KZ=\left(k\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(l\underset{\dot{}}{·}Y\right)\right)$$