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 ⊢ V = Base W
lspval.s ⊢ S = LSubSp ⁡ W
lspval.n ⊢ N = LSpan ⁡ W
Assertion lspsncl ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X ∈ S

Proof

Step Hyp Ref Expression
1 lspval.v ⊢ V = Base W
2 lspval.s ⊢ S = LSubSp ⁡ W
3 lspval.n ⊢ N = LSpan ⁡ W
4 snssi ⊢ X ∈ V → X ⊆ V
5 1 2 3 lspcl ⊢ W ∈ LMod ∧ X ⊆ V → N ⁡ X ∈ S
6 4 5 sylan2 ⊢ W ∈ LMod ∧ X ∈ V → N ⁡ X ∈ S