Metamath Proof Explorer


Theorem lspsnel5a

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

Ref Expression
Hypotheses lspsnel5a.s 𝑆 = ( LSubSp ‘ 𝑊 )
lspsnel5a.n 𝑁 = ( LSpan ‘ 𝑊 )
lspsnel5a.w ( 𝜑𝑊 ∈ LMod )
lspsnel5a.a ( 𝜑𝑈𝑆 )
lspsnel5a.x ( 𝜑𝑋𝑈 )
Assertion lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )

Proof

Step Hyp Ref Expression
1 lspsnel5a.s 𝑆 = ( LSubSp ‘ 𝑊 )
2 lspsnel5a.n 𝑁 = ( LSpan ‘ 𝑊 )
3 lspsnel5a.w ( 𝜑𝑊 ∈ LMod )
4 lspsnel5a.a ( 𝜑𝑈𝑆 )
5 lspsnel5a.x ( 𝜑𝑋𝑈 )
6 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 6 1 lssel ( ( 𝑈𝑆𝑋𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
8 4 5 7 syl2anc ( 𝜑𝑋 ∈ ( Base ‘ 𝑊 ) )
9 6 1 2 3 4 8 lspsnel5 ( 𝜑 → ( 𝑋𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
10 5 9 mpbid ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )