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

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 ellspsn5b.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 1 2 3 4 5 ellspsn6 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )
8 6 7 mpbirand ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )