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

Metamath Proof Explorer

Theorem lspssv

Description: A span is a set of vectors. (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lspss.v ⊢ V = Base W
lspss.n ⊢ N = LSpan ⁡ W
Assertion lspssv ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U ⊆ V

Proof

Step Hyp Ref Expression
1 lspss.v ⊢ V = Base W
2 lspss.n ⊢ N = LSpan ⁡ W
3 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
4 1 3 2 lspcl ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U ∈ LSubSp ⁡ W
5 1 3 lssss ⊢ N ⁡ U ∈ LSubSp ⁡ W → N ⁡ U ⊆ V
6 4 5 syl ⊢ W ∈ LMod ∧ U ⊆ V → N ⁡ U ⊆ V