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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
ellspsn5b.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
ellspsn5b.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
ellspsn5b.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ellspsn5b.a ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion ellspsn6 ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 ellspsn5b.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 ellspsn5b.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 ellspsn5b.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 ellspsn5b.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 ellspsn5b.a ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 1 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
7 5 6 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
11 2 3 lspsnss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
12 8 9 10 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
13 7 12 jca ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
14 1 3 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
15 4 14 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
16 ssel ⊢ ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) → 𝑋 ∈ 𝑈 ) )
17 15 16 syl5com ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 → 𝑋 ∈ 𝑈 ) )
18 17 impr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) → 𝑋 ∈ 𝑈 )
19 13 18 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )