Theorem lsppreli

Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	lsppreli.v	$$⊢V={\mathrm{Base}}_W$$
	lsppreli.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lsppreli.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lsppreli.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lsppreli.k	$$⊢K={\mathrm{Base}}_F$$
	lsppreli.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsppreli.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lsppreli.a	$$⊢\phi \to A\in K$$
	lsppreli.b	$$⊢\phi \to B\in K$$
	lsppreli.x	$$⊢\phi \to X\in V$$
	lsppreli.y	$$⊢\phi \to Y\in V$$
Assertion	lsppreli	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\in N\left(\left\{X,Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsppreli.v	$$⊢V={\mathrm{Base}}_W$$
2		lsppreli.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lsppreli.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		lsppreli.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		lsppreli.k	$$⊢K={\mathrm{Base}}_F$$
6		lsppreli.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
7		lsppreli.w	$$⊢\phi \to W\in \mathrm{LMod}$$
8		lsppreli.a	$$⊢\phi \to A\in K$$
9		lsppreli.b	$$⊢\phi \to B\in K$$
10		lsppreli.x	$$⊢\phi \to X\in V$$
11		lsppreli.y	$$⊢\phi \to Y\in V$$
12	1 6	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
13	7 10 12	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
14	1 6	lspsnsubg	$$⊢\left(W\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
15	7 11 14	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(W\right)$$
16	1 3 4 5 6 7 8 10	ellspsni	$$⊢\phi \to A\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)$$
17	1 3 4 5 6 7 9 11	ellspsni	$$⊢\phi \to B\underset{\dot{}}{·}Y\in N\left(\left\{Y\right\}\right)$$
18		eqid	$$⊢\mathrm{LSSum}\left(W\right)=\mathrm{LSSum}\left(W\right)$$
19	2 18	lsmelvali	$$⊢\left(\left(N\left(\left\{X\right\}\right)\in \mathrm{SubGrp}\left(W\right)\wedge N\left(\left\{Y\right\}\right)\in \mathrm{SubGrp}\left(W\right)\right)\wedge \left(A\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)\wedge B\underset{\dot{}}{·}Y\in N\left(\left\{Y\right\}\right)\right)\right)\to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\in \left(N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)\right)$$
20	13 15 16 17 19	syl22anc	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\in \left(N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)\right)$$
21	1 6 18 7 10 11	lsmpr	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)=N\left(\left\{X\right\}\right)\mathrm{LSSum}\left(W\right)N\left(\left\{Y\right\}\right)$$
22	20 21	eleqtrrd	$$⊢\phi \to \left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}\left(B\underset{\dot{}}{·}Y\right)\in N\left(\left\{X,Y\right\}\right)$$