Theorem ellspsni

Description: A scalar product with a vector belongs to the span of its singleton. ( spansnmul analog.) (Contributed by NM, 2-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lspsnvsel.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnvsel.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		lspsnvsel.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lspsnvsel.k	$$⊢K={\mathrm{Base}}_F$$
5		lspsnvsel.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
6		lspsnvsel.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lspsnvsel.a	$$⊢\phi \to A\in K$$
8		lspsnvsel.x	$$⊢\phi \to X\in V$$
9		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
10	1 9 5	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
11	6 8 10	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(W\right)$$
12	1 5	lspsnid	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to X\in N\left(\left\{X\right\}\right)$$
13	6 8 12	syl2anc	$$⊢\phi \to X\in N\left(\left\{X\right\}\right)$$
14	3 2 4 9	lssvscl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(W\right)\right)\wedge \left(A\in K\wedge X\in N\left(\left\{X\right\}\right)\right)\right)\to A\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)$$
15	6 11 7 13 14	syl22anc	$$⊢\phi \to A\underset{\dot{}}{·}X\in N\left(\left\{X\right\}\right)$$