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=BaseW
lspsnel5.s S=LSubSpW
lspsnel5.n N=LSpanW
lspsnel5.w φWLMod
lspsnel5.a φUS
lspsnel5.x φXV
Assertion lspsnel5 φXUNXU

Proof

Step Hyp Ref Expression
1 lspsnel5.v V=BaseW
2 lspsnel5.s S=LSubSpW
3 lspsnel5.n N=LSpanW
4 lspsnel5.w φWLMod
5 lspsnel5.a φUS
6 lspsnel5.x φXV
7 1 2 3 4 5 lspsnel6 φXUXVNXU
8 6 7 mpbirand φXUNXU