This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑈 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑈 = ( 𝑘 · 𝑋 ) ) )