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 = Base W
lspsnel5.s S = LSubSp W
lspsnel5.n N = LSpan W
lspsnel5.w φ W LMod
lspsnel5.a φ U S
lspsnel5.x φ X V
Assertion lspsnel5 φ X U N X U


Step Hyp Ref Expression
1 lspsnel5.v V = Base W
2 lspsnel5.s S = LSubSp W
3 lspsnel5.n N = LSpan W
4 lspsnel5.w φ W LMod
5 lspsnel5.a φ U S
6 lspsnel5.x φ X V
7 1 2 3 4 5 lspsnel6 φ X U X V N X U
8 6 7 mpbirand φ X U N X U