Theorem lspsnel5

Description: Relationship between a vector and the 1-dim (or 0-dim) subspace it generates. (Contributed by NM, 8-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		lspsnel5.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsnel5.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lspsnel5.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsnel5.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
5		lspsnel5.a	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6		lspsnel5.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7	1 2 3 4 5	lspsnel6	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )
8	6 7	mpbirand	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )