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

Metamath Proof Explorer

Theorem ellspsn5b

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 ellspsn5b.v ⊢ V = Base W
2 ellspsn5b.s ⊢ S = LSubSp ⁡ W
3 ellspsn5b.n ⊢ N = LSpan ⁡ W
4 ellspsn5b.w ⊢ φ → W ∈ LMod
5 ellspsn5b.a ⊢ φ → U ∈ S
6 ellspsn5b.x ⊢ φ → X ∈ V
7 1 2 3 4 5 ellspsn6 ⊢ φ → X ∈ U ↔ X ∈ V ∧ N ⁡ X ⊆ U
8 6 7 mpbirand ⊢ φ → X ∈ U ↔ N ⁡ X ⊆ U