Metamath Proof Explorer


Theorem lspsnel

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