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