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	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )