# Metamath Proof Explorer

## Theorem lspsnel6

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

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}$
Assertion lspsnel6 ${⊢}{\phi }\to \left({X}\in {U}↔\left({X}\in {V}\wedge {N}\left(\left\{{X}\right\}\right)\subseteq {U}\right)\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 1 2 lssel ${⊢}\left({U}\in {S}\wedge {X}\in {U}\right)\to {X}\in {V}$
7 5 6 sylan ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {X}\in {V}$
8 4 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {W}\in \mathrm{LMod}$
9 5 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {U}\in {S}$
10 simpr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {X}\in {U}$
11 2 3 lspsnss ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\wedge {X}\in {U}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {U}$
12 8 9 10 11 syl3anc ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {U}$
13 7 12 jca ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to \left({X}\in {V}\wedge {N}\left(\left\{{X}\right\}\right)\subseteq {U}\right)$
14 1 3 lspsnid ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {X}\in {N}\left(\left\{{X}\right\}\right)$
15 4 14 sylan ${⊢}\left({\phi }\wedge {X}\in {V}\right)\to {X}\in {N}\left(\left\{{X}\right\}\right)$
16 ssel ${⊢}{N}\left(\left\{{X}\right\}\right)\subseteq {U}\to \left({X}\in {N}\left(\left\{{X}\right\}\right)\to {X}\in {U}\right)$
17 15 16 syl5com ${⊢}\left({\phi }\wedge {X}\in {V}\right)\to \left({N}\left(\left\{{X}\right\}\right)\subseteq {U}\to {X}\in {U}\right)$
18 17 impr ${⊢}\left({\phi }\wedge \left({X}\in {V}\wedge {N}\left(\left\{{X}\right\}\right)\subseteq {U}\right)\right)\to {X}\in {U}$
19 13 18 impbida ${⊢}{\phi }\to \left({X}\in {U}↔\left({X}\in {V}\wedge {N}\left(\left\{{X}\right\}\right)\subseteq {U}\right)\right)$