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 ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )