Proof of Theorem nn0gsumfz
Step | Hyp | Ref
| Expression |
1 | | nn0gsumfz.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
2 | | nn0gsumfz.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
3 | 2 | fvexi 6448 |
. . . 4
⊢ 0 ∈
V |
4 | 1, 3 | jctir 518 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ 0 ∈
V)) |
5 | | nn0gsumfz.y |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
6 | | fsuppmapnn0ub 13090 |
. . 3
⊢ ((𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ 0 ∈ V) → (𝐹 finSupp 0 → ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ))) |
7 | 4, 5, 6 | sylc 65 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 )) |
8 | | eqidd 2827 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠))) |
9 | | simpr 479 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 )) |
10 | | nn0gsumfz.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
11 | | nn0gsumfz.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ CMnd) |
12 | 11 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐺 ∈ CMnd) |
13 | 1 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
14 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
15 | | eqid 2826 |
. . . . . . 7
⊢ (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) |
16 | 10, 2, 12, 13, 14, 15 | fsfnn0gsumfsffz 18733 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠))))) |
17 | 16 | imp 397 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) |
18 | 13 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
19 | | fz0ssnn0 12730 |
. . . . . . 7
⊢
(0...𝑠) ⊆
ℕ0 |
20 | | elmapssres 8148 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ (0...𝑠) ⊆ ℕ0) → (𝐹 ↾ (0...𝑠)) ∈ (𝐵 ↑𝑚 (0...𝑠))) |
21 | 18, 19, 20 | sylancl 582 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐹 ↾ (0...𝑠)) ∈ (𝐵 ↑𝑚 (0...𝑠))) |
22 | | eqeq1 2830 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → (𝑓 = (𝐹 ↾ (0...𝑠)) ↔ (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)))) |
23 | | oveq2 6914 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) |
24 | 23 | eqeq2d 2836 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → ((𝐺 Σg 𝐹) = (𝐺 Σg 𝑓) ↔ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠))))) |
25 | 22, 24 | 3anbi13d 1568 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → ((𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)) ↔ ((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))))) |
26 | 25 | adantl 475 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) ∧ 𝑓 = (𝐹 ↾ (0...𝑠))) → ((𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)) ↔ ((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))))) |
27 | 21, 26 | rspcedv 3531 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
28 | 8, 9, 17, 27 | mp3and 1594 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))) |
29 | 28 | ex 403 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
30 | 29 | reximdva 3226 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) → ∃𝑠 ∈ ℕ0
∃𝑓 ∈ (𝐵 ↑𝑚
(0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
31 | 7, 30 | mpd 15 |
1
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))) |