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

Proof

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