This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspsncl

Description: The span of a singleton is a subspace (frequently used special case of lspcl ). (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspval.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 snssi ⊢ ( 𝑋 ∈ 𝑉 → { 𝑋 } ⊆ 𝑉 )
5 1 2 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )
6 4 5 sylan2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ 𝑆 )