# Metamath Proof Explorer

## Theorem lspsnel5

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014)

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

### Proof

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