Theorem ellspsn6

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

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

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	1 2	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
7	5 6	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
11	2 3	lspsnss	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
12	8 9 10 11	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 )
13	7 12	jca	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
14	1 3	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
15	4 14	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
16		ssel	⊢ ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) → 𝑋 ∈ 𝑈 ) )
17	15 16	syl5com	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 → 𝑋 ∈ 𝑈 ) )
18	17	impr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) → 𝑋 ∈ 𝑈 )
19	13 18	impbida	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )