# Metamath Proof Explorer

## 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)↔\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)↔\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)$