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 | |- ( ph -> W e. LMod ) |
||
lspsnel3.u | |- ( ph -> U e. S ) |
||
lspsnel3.x | |- ( ph -> X e. U ) |
||
lspsnel3.y | |- ( ph -> Y e. ( N ` { X } ) ) |
||
Assertion | lspsnel3 | |- ( ph -> Y e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspsnss.s | |- S = ( LSubSp ` W ) |
|
2 | lspsnss.n | |- N = ( LSpan ` W ) |
|
3 | lspsnel3.w | |- ( ph -> W e. LMod ) |
|
4 | lspsnel3.u | |- ( ph -> U e. S ) |
|
5 | lspsnel3.x | |- ( ph -> X e. U ) |
|
6 | lspsnel3.y | |- ( ph -> Y e. ( N ` { X } ) ) |
|
7 | 1 2 | lspsnss | |- ( ( W e. LMod /\ U e. S /\ X e. U ) -> ( N ` { X } ) C_ U ) |
8 | 3 4 5 7 | syl3anc | |- ( ph -> ( N ` { X } ) C_ U ) |
9 | 8 6 | sseldd | |- ( ph -> Y e. U ) |