Metamath Proof Explorer


Theorem lspsnel3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn3 analog.) (Contributed by NM, 4-Jul-2014)

Ref Expression
Hypotheses lspsnss.s S = LSubSp W
lspsnss.n N = LSpan W
lspsnel3.w φ W LMod
lspsnel3.u φ U S
lspsnel3.x φ X U
lspsnel3.y φ Y N X
Assertion lspsnel3 φ Y U

Proof

Step Hyp Ref Expression
1 lspsnss.s S = LSubSp W
2 lspsnss.n N = LSpan W
3 lspsnel3.w φ W LMod
4 lspsnel3.u φ U S
5 lspsnel3.x φ X U
6 lspsnel3.y φ Y N X
7 1 2 lspsnss W LMod U S X U N X U
8 3 4 5 7 syl3anc φ N X U
9 8 6 sseldd φ Y U