Metamath Proof Explorer


Theorem lspsnss

Description: The span of the singleton of a subspace member is included in the subspace. ( spansnss analog.) (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 4-Sep-2014)

Ref Expression
Hypotheses lspsnss.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnss.n 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsnss ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )

Proof

Step Hyp Ref Expression
1 lspsnss.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lspsnss.n 𝑁 = ( LSpan ‘ 𝑊 )
3 snssi ( 𝑋𝑈 → { 𝑋 } ⊆ 𝑈 )
4 1 2 lspssp ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆 ∧ { 𝑋 } ⊆ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
5 3 4 syl3an3 ( ( 𝑊 ∈ LMod ∧ 𝑈𝑆𝑋𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )