Theorem lspsnid

Description: A vector belongs to the span of its singleton. ( spansnid analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspsnid.v	$$⊢V={\mathrm{Base}}_W$$
	lspsnid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lspsnid	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to X\in N\left(\left\{X\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lspsnid.v	$$⊢V={\mathrm{Base}}_W$$
2		lspsnid.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		snssi	$$⊢X\in V\to \left\{X\right\}\subseteq V$$
4	1 2	lspssid	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{X\right\}\subseteq V\right)\to \left\{X\right\}\subseteq N\left(\left\{X\right\}\right)$$
5	3 4	sylan2	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \left\{X\right\}\subseteq N\left(\left\{X\right\}\right)$$
6		snssg	$$⊢X\in V\to \left(X\in N\left(\left\{X\right\}\right)\leftrightarrow \left\{X\right\}\subseteq N\left(\left\{X\right\}\right)\right)$$
7	6	adantl	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \left(X\in N\left(\left\{X\right\}\right)\leftrightarrow \left\{X\right\}\subseteq N\left(\left\{X\right\}\right)\right)$$
8	5 7	mpbird	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to X\in N\left(\left\{X\right\}\right)$$