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

Metamath Proof Explorer

Theorem ellspsn6

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

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
Assertion ellspsn6 ⊢ φ → X ∈ U ↔ X ∈ V ∧ 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 1 2 lssel ⊢ U ∈ S ∧ X ∈ U → X ∈ V
7 5 6 sylan ⊢ φ ∧ X ∈ U → X ∈ V
8 4 adantr ⊢ φ ∧ X ∈ U → W ∈ LMod
9 5 adantr ⊢ φ ∧ X ∈ U → U ∈ S
10 simpr ⊢ φ ∧ X ∈ U → X ∈ U
11 2 3 lspsnss ⊢ W ∈ LMod ∧ U ∈ S ∧ X ∈ U → N ⁡ X ⊆ U
12 8 9 10 11 syl3anc ⊢ φ ∧ X ∈ U → N ⁡ X ⊆ U
13 7 12 jca ⊢ φ ∧ X ∈ U → X ∈ V ∧ N ⁡ X ⊆ U
14 1 3 lspsnid ⊢ W ∈ LMod ∧ X ∈ V → X ∈ N ⁡ X
15 4 14 sylan ⊢ φ ∧ X ∈ V → X ∈ N ⁡ X
16 ssel ⊢ N ⁡ X ⊆ U → X ∈ N ⁡ X → X ∈ U
17 15 16 syl5com ⊢ φ ∧ X ∈ V → N ⁡ X ⊆ U → X ∈ U
18 17 impr ⊢ φ ∧ X ∈ V ∧ N ⁡ X ⊆ U → X ∈ U
19 13 18 impbida ⊢ φ → X ∈ U ↔ X ∈ V ∧ N ⁡ X ⊆ U