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