Theorem ellspsn4

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. ( elspansn4 analog.) (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	ellspsn4.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ellspsn4.o	⊢ 0 = ( 0g ‘ 𝑊 )
	ellspsn4.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	ellspsn4.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	ellspsn4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	ellspsn4.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	ellspsn4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	ellspsn4.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
	ellspsn4.z	⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion	ellspsn4	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ellspsn4.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		ellspsn4.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		ellspsn4.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4		ellspsn4.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		ellspsn4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		ellspsn4.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
7		ellspsn4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8		ellspsn4.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
9		ellspsn4.z	⊢ ( 𝜑 → 𝑌 ≠ 0 )
10		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11	5 10	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
16	3 4 12 13 14 15	ellspsn3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
17	11	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑈 ) → 𝑊 ∈ LMod )
18	6	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
20	1 4	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
21	11 7 20	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
22	1 2 4 5 7 8 9	lspsneleq	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )
23	21 22	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
25	3 4 17 18 19 24	ellspsn3	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
26	16 25	impbida	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ 𝑌 ∈ 𝑈 ) )