Step |
Hyp |
Ref |
Expression |
1 |
|
ellspd.n |
⊢ 𝑁 = ( LSpan ‘ 𝑀 ) |
2 |
|
ellspd.v |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
3 |
|
ellspd.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
4 |
|
ellspd.s |
⊢ 𝑆 = ( Scalar ‘ 𝑀 ) |
5 |
|
ellspd.z |
⊢ 0 = ( 0g ‘ 𝑆 ) |
6 |
|
ellspd.t |
⊢ · = ( ·𝑠 ‘ 𝑀 ) |
7 |
|
elfilspd.f |
⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 ) |
8 |
|
elfilspd.m |
⊢ ( 𝜑 → 𝑀 ∈ LMod ) |
9 |
|
elfilspd.i |
⊢ ( 𝜑 → 𝐼 ∈ Fin ) |
10 |
1 2 3 4 5 6 7 8 9
|
ellspd |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) ) |
11 |
|
elmapi |
⊢ ( 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ 𝐾 ) |
12 |
11
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑓 : 𝐼 ⟶ 𝐾 ) |
13 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝐼 ∈ Fin ) |
14 |
5
|
fvexi |
⊢ 0 ∈ V |
15 |
14
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 0 ∈ V ) |
16 |
12 13 15
|
fdmfifsupp |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → 𝑓 finSupp 0 ) |
17 |
16
|
biantrurd |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ) → ( 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) ) |
18 |
17
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) ( 𝑓 finSupp 0 ∧ 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) ) |
19 |
10 18
|
bitr4d |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ ( 𝐹 “ 𝐼 ) ) ↔ ∃ 𝑓 ∈ ( 𝐾 ↑m 𝐼 ) 𝑋 = ( 𝑀 Σg ( 𝑓 ∘f · 𝐹 ) ) ) ) |