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

Metamath Proof Explorer

Theorem lsptpcl

Description: The span of an unordered triple is a subspace (frequently used special case of lspcl ). (Contributed by NM, 22-May-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
lsptpcl.z ⊢ φ → Z ∈ V
Assertion lsptpcl ⊢ φ → N ⁡ X Y Z ∈ 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 lsptpcl.z ⊢ φ → Z ∈ V
8 df-tp ⊢ X Y Z = X Y ∪ Z
9 5 6 prssd ⊢ φ → X Y ⊆ V
10 7 snssd ⊢ φ → Z ⊆ V
11 9 10 unssd ⊢ φ → X Y ∪ Z ⊆ V
12 8 11 eqsstrid ⊢ φ → X Y Z ⊆ V
13 1 2 3 lspcl ⊢ W ∈ LMod ∧ X Y Z ⊆ V → N ⁡ X Y Z ∈ S
14 4 12 13 syl2anc ⊢ φ → N ⁡ X Y Z ∈ S