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	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lspsnss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	ellspsn3.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ellspsn3.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	ellspsn3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	ellspsn3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
Assertion	ellspsn3	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lspsnss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
2		lspsnss.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3		ellspsn3.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		ellspsn3.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
5		ellspsn3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
6		ellspsn3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
7	1 2	lspsnss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
8	3 4 5 7	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
9	8 6	sseldd	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )