# Metamath Proof Explorer

## Theorem lspsnel5a

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015)

Ref Expression
Hypotheses lspsnel5a.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lspsnel5a.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspsnel5a.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lspsnel5a.a ${⊢}{\phi }\to {U}\in {S}$
lspsnel5a.x ${⊢}{\phi }\to {X}\in {U}$
Assertion lspsnel5a ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\subseteq {U}$

### Proof

Step Hyp Ref Expression
1 lspsnel5a.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
2 lspsnel5a.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lspsnel5a.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
4 lspsnel5a.a ${⊢}{\phi }\to {U}\in {S}$
5 lspsnel5a.x ${⊢}{\phi }\to {X}\in {U}$
6 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
7 6 1 lssel ${⊢}\left({U}\in {S}\wedge {X}\in {U}\right)\to {X}\in {\mathrm{Base}}_{{W}}$
8 4 5 7 syl2anc ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{{W}}$
9 6 1 2 3 4 8 lspsnel5 ${⊢}{\phi }\to \left({X}\in {U}↔{N}\left(\left\{{X}\right\}\right)\subseteq {U}\right)$
10 5 9 mpbid ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\subseteq {U}$