Theorem ellspsn3

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 )
	ellspsn3.w	|- ( ph -> W e. LMod )
	ellspsn3.u	|- ( ph -> U e. S )
	ellspsn3.x	|- ( ph -> X e. U )
	ellspsn3.y	|- ( ph -> Y e. ( N ` { X } ) )
Assertion	ellspsn3	|- ( ph -> Y e. U )

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	|- S = ( LSubSp ` W )
2		lspsnss.n	|- N = ( LSpan ` W )
3		ellspsn3.w	|- ( ph -> W e. LMod )
4		ellspsn3.u	|- ( ph -> U e. S )
5		ellspsn3.x	|- ( ph -> X e. U )
6		ellspsn3.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 )