Proof of Theorem nn0gsumfz
Step | Hyp | Ref
| Expression |
1 | | nn0gsumfz.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
2 | | nn0gsumfz.0 |
. . . . 5
⊢ 0 =
(0g‘𝐺) |
3 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝐺) ∈ V |
4 | 2, 3 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
5 | 1, 4 | jctir 559 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ 0 ∈
V)) |
6 | | nn0gsumfz.y |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
7 | | fsuppmapnn0ub 12657 |
. . 3
⊢ ((𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ 0 ∈ V) → (𝐹 finSupp 0 → ∃𝑠 ∈ ℕ0
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ))) |
8 | 5, 6, 7 | sylc 63 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 )) |
9 | | eqidd 2611 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠))) |
10 | | simpr 476 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 )) |
11 | | nn0gsumfz.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
12 | | nn0gsumfz.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ CMnd) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐺 ∈ CMnd) |
14 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
15 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) → 𝑠 ∈
ℕ0) |
16 | | eqid 2610 |
. . . . . . 7
⊢ (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) |
17 | 11, 2, 13, 14, 15, 16 | fsfnn0gsumfsffz 18202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠))))) |
18 | 17 | imp 444 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐺 Σg
𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) |
19 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
20 | | fz0ssnn0 12304 |
. . . . . . 7
⊢
(0...𝑠) ⊆
ℕ0 |
21 | | elmapssres 7768 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐵 ↑𝑚
ℕ0) ∧ (0...𝑠) ⊆ ℕ0) → (𝐹 ↾ (0...𝑠)) ∈ (𝐵 ↑𝑚 (0...𝑠))) |
22 | 19, 20, 21 | sylancl 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (𝐹 ↾ (0...𝑠)) ∈ (𝐵 ↑𝑚 (0...𝑠))) |
23 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → (𝑓 = (𝐹 ↾ (0...𝑠)) ↔ (𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)))) |
24 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → (𝐺 Σg 𝑓) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) |
25 | 24 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → ((𝐺 Σg 𝐹) = (𝐺 Σg 𝑓) ↔ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠))))) |
26 | 23, 25 | 3anbi13d 1393 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ↾ (0...𝑠)) → ((𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)) ↔ ((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))))) |
27 | 26 | adantl 481 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) ∧ 𝑓 = (𝐹 ↾ (0...𝑠))) → ((𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)) ↔ ((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))))) |
28 | 22, 27 | rspcedv 3286 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → (((𝐹 ↾ (0...𝑠)) = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ↾ (0...𝑠)))) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
29 | 9, 10, 18, 28 | mp3and 1419 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧
∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 )) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))) |
30 | 29 | ex 449 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝑠 <
𝑥 → (𝐹‘𝑥) = 0 ) → ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
31 | 30 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0
(𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) → ∃𝑠 ∈ ℕ0
∃𝑓 ∈ (𝐵 ↑𝑚
(0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)))) |
32 | 8, 31 | mpd 15 |
1
⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑𝑚 (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))) |