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

Metamath Proof Explorer

Theorem ellspsn5

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 20-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 ellspsn5.s ⊢ S = LSubSp ⁡ W
2 ellspsn5.n ⊢ N = LSpan ⁡ W
3 ellspsn5.w ⊢ φ → W ∈ LMod
4 ellspsn5.a ⊢ φ → U ∈ S
5 ellspsn5.x ⊢ φ → X ∈ U
6 eqid ⊢ Base W = Base W
7 6 1 lssel ⊢ U ∈ S ∧ X ∈ U → X ∈ Base W
8 4 5 7 syl2anc ⊢ φ → X ∈ Base W
9 6 1 2 3 4 8 ellspsn5b ⊢ φ → X ∈ U ↔ N ⁡ X ⊆ U
10 5 9 mpbid ⊢ φ → N ⁡ X ⊆ U