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

Metamath Proof Explorer

Theorem lspprss

Description: The span of a pair of vectors in a subspace belongs to the subspace. (Contributed by NM, 12-Jan-2015)

Ref Expression
Hypotheses lspprss.s ⊢ S = LSubSp ⁡ W
lspprss.n ⊢ N = LSpan ⁡ W
lspprss.w ⊢ φ → W ∈ LMod
lspprss.u ⊢ φ → U ∈ S
lspprss.x ⊢ φ → X ∈ U
lspprss.y ⊢ φ → Y ∈ U
Assertion lspprss ⊢ φ → N ⁡ X Y ⊆ U

Proof

Step Hyp Ref Expression
1 lspprss.s ⊢ S = LSubSp ⁡ W
2 lspprss.n ⊢ N = LSpan ⁡ W
3 lspprss.w ⊢ φ → W ∈ LMod
4 lspprss.u ⊢ φ → U ∈ S
5 lspprss.x ⊢ φ → X ∈ U
6 lspprss.y ⊢ φ → Y ∈ U
7 5 6 prssd ⊢ φ → X Y ⊆ U
8 1 2 lspssp ⊢ W ∈ LMod ∧ U ∈ S ∧ X Y ⊆ U → N ⁡ X Y ⊆ U
9 3 4 7 8 syl3anc ⊢ φ → N ⁡ X Y ⊆ U