Step | Hyp | Ref
| Expression |
1 | | df-fwddif 34455 |
. . . 4
⊢ △
= (𝑓 ∈ (ℂ
↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)))) |
2 | | dmeq 5810 |
. . . . . 6
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
3 | 2 | eleq2d 2826 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑦 + 1) ∈ dom 𝑓 ↔ (𝑦 + 1) ∈ dom 𝐹)) |
4 | 2, 3 | rabeqbidv 3419 |
. . . . 5
⊢ (𝑓 = 𝐹 → {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} = {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹}) |
5 | | fveq1 6768 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 1)) = (𝐹‘(𝑥 + 1))) |
6 | | fveq1 6768 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) |
7 | 5, 6 | oveq12d 7287 |
. . . . 5
⊢ (𝑓 = 𝐹 → ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)) = ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) |
8 | 4, 7 | mpteq12dv 5170 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))) = (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
9 | | fwddifval.2 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
10 | | fwddifval.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
11 | | cnex 10951 |
. . . . . 6
⊢ ℂ
∈ V |
12 | | elpm2r 8614 |
. . . . . 6
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
13 | 11, 11, 12 | mpanl12 699 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
14 | 9, 10, 13 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
15 | 9 | fdmd 6608 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
16 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℂ ∈
V) |
17 | 16, 10 | ssexd 5252 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
18 | 15, 17 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → dom 𝐹 ∈ V) |
19 | | rabexg 5259 |
. . . . 5
⊢ (dom
𝐹 ∈ V → {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ∈ V) |
20 | | mptexg 7092 |
. . . . 5
⊢ ({𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ∈ V → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) ∈ V) |
21 | 18, 19, 20 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) ∈ V) |
22 | 1, 8, 14, 21 | fvmptd3 6893 |
. . 3
⊢ (𝜑 → ( △ ‘𝐹) = (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
23 | 15 | eleq2d 2826 |
. . . . 5
⊢ (𝜑 → ((𝑦 + 1) ∈ dom 𝐹 ↔ (𝑦 + 1) ∈ 𝐴)) |
24 | 15, 23 | rabeqbidv 3419 |
. . . 4
⊢ (𝜑 → {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} = {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴}) |
25 | 24 | mpteq1d 5174 |
. . 3
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ dom 𝐹 ∣ (𝑦 + 1) ∈ dom 𝐹} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥))) = (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
26 | 22, 25 | eqtrd 2780 |
. 2
⊢ (𝜑 → ( △ ‘𝐹) = (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↦ ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)))) |
27 | | fvoveq1 7292 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 1)) = (𝐹‘(𝑋 + 1))) |
28 | | fveq2 6769 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
29 | 27, 28 | oveq12d 7287 |
. . 3
⊢ (𝑥 = 𝑋 → ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |
30 | 29 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝐹‘(𝑥 + 1)) − (𝐹‘𝑥)) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |
31 | | fwddifval.3 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
32 | | fwddifval.4 |
. . 3
⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴) |
33 | | oveq1 7276 |
. . . . 5
⊢ (𝑦 = 𝑋 → (𝑦 + 1) = (𝑋 + 1)) |
34 | 33 | eleq1d 2825 |
. . . 4
⊢ (𝑦 = 𝑋 → ((𝑦 + 1) ∈ 𝐴 ↔ (𝑋 + 1) ∈ 𝐴)) |
35 | 34 | elrab 3626 |
. . 3
⊢ (𝑋 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴} ↔ (𝑋 ∈ 𝐴 ∧ (𝑋 + 1) ∈ 𝐴)) |
36 | 31, 32, 35 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ 𝐴 ∣ (𝑦 + 1) ∈ 𝐴}) |
37 | | ovexd 7304 |
. 2
⊢ (𝜑 → ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋)) ∈ V) |
38 | 26, 30, 36, 37 | fvmptd 6877 |
1
⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) |