Theorem ellspsn

Description: Member of span of the singleton of a vector. ( elspansn analog.) (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lspsn.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lspsn.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lspsn.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsn.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lspsn.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion	ellspsn	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lspsn.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lspsn.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		lspsn.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lspsn.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		lspsn.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6	1 2 3 4 5	lspsn	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } )
7	6	eleq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ 𝑈 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ) )
8		id	⊢ ( 𝑈 = ( 𝑘 · 𝑋 ) → 𝑈 = ( 𝑘 · 𝑋 ) )
9		ovex	⊢ ( 𝑘 · 𝑋 ) ∈ V
10	8 9	eqeltrdi	⊢ ( 𝑈 = ( 𝑘 · 𝑋 ) → 𝑈 ∈ V )
11	10	rexlimivw	⊢ ( ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) → 𝑈 ∈ V )
12		eqeq1	⊢ ( 𝑣 = 𝑈 → ( 𝑣 = ( 𝑘 · 𝑋 ) ↔ 𝑈 = ( 𝑘 · 𝑋 ) ) )
13	12	rexbidv	⊢ ( 𝑣 = 𝑈 → ( ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) ↔ ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) ) )
14	11 13	elab3	⊢ ( 𝑈 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐾 𝑣 = ( 𝑘 · 𝑋 ) } ↔ ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) )
15	7 14	bitrdi	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) ) )