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
|- ( 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 )

Proof

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 )