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

Metamath Proof Explorer

Theorem lspprcl

Description: The span of a pair is a subspace (frequently used special case of lspcl ). (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lspval.v ⊢ V = Base W
lspval.s ⊢ S = LSubSp ⁡ W
lspval.n ⊢ N = LSpan ⁡ W
lspprcl.w ⊢ φ → W ∈ LMod
lspprcl.x ⊢ φ → X ∈ V
lspprcl.y ⊢ φ → Y ∈ V
Assertion lspprcl ⊢ φ → N ⁡ X Y ∈ 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 lspprcl.w ⊢ φ → W ∈ LMod
5 lspprcl.x ⊢ φ → X ∈ V
6 lspprcl.y ⊢ φ → Y ∈ V
7 5 6 prssd ⊢ φ → X Y ⊆ V
8 1 2 3 lspcl ⊢ W ∈ LMod ∧ X Y ⊆ V → N ⁡ X Y ∈ S
9 4 7 8 syl2anc ⊢ φ → N ⁡ X Y ∈ S