Theorem ellspsn5

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

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

Proof

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