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 | ||
lspsnss.n | |||
lspsnel3.w | |||
lspsnel3.u | |||
lspsnel3.x | |||
lspsnel3.y | |||
Assertion | lspsnel3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnss.s | ||
2 | lspsnss.n | ||
3 | lspsnel3.w | ||
4 | lspsnel3.u | ||
5 | lspsnel3.x | ||
6 | lspsnel3.y | ||
7 | 1 2 | lspsnss | |
8 | 3 4 5 7 | syl3anc | |
9 | 8 6 | sseldd |