Step | Hyp | Ref
| Expression |
1 | | df-fwddif 34797 |
. . . 4
β’ β³
= (π β (β
βpm β) β¦ (π₯ β {π¦ β dom π β£ (π¦ + 1) β dom π} β¦ ((πβ(π₯ + 1)) β (πβπ₯)))) |
2 | | dmeq 5863 |
. . . . . 6
β’ (π = πΉ β dom π = dom πΉ) |
3 | 2 | eleq2d 2820 |
. . . . . 6
β’ (π = πΉ β ((π¦ + 1) β dom π β (π¦ + 1) β dom πΉ)) |
4 | 2, 3 | rabeqbidv 3423 |
. . . . 5
β’ (π = πΉ β {π¦ β dom π β£ (π¦ + 1) β dom π} = {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ}) |
5 | | fveq1 6845 |
. . . . . 6
β’ (π = πΉ β (πβ(π₯ + 1)) = (πΉβ(π₯ + 1))) |
6 | | fveq1 6845 |
. . . . . 6
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
7 | 5, 6 | oveq12d 7379 |
. . . . 5
β’ (π = πΉ β ((πβ(π₯ + 1)) β (πβπ₯)) = ((πΉβ(π₯ + 1)) β (πΉβπ₯))) |
8 | 4, 7 | mpteq12dv 5200 |
. . . 4
β’ (π = πΉ β (π₯ β {π¦ β dom π β£ (π¦ + 1) β dom π} β¦ ((πβ(π₯ + 1)) β (πβπ₯))) = (π₯ β {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ} β¦ ((πΉβ(π₯ + 1)) β (πΉβπ₯)))) |
9 | | fwddifval.2 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
10 | | fwddifval.1 |
. . . . 5
β’ (π β π΄ β β) |
11 | | cnex 11140 |
. . . . . 6
β’ β
β V |
12 | | elpm2r 8789 |
. . . . . 6
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
13 | 11, 11, 12 | mpanl12 701 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
14 | 9, 10, 13 | syl2anc 585 |
. . . 4
β’ (π β πΉ β (β βpm
β)) |
15 | 9 | fdmd 6683 |
. . . . . 6
β’ (π β dom πΉ = π΄) |
16 | 11 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
17 | 16, 10 | ssexd 5285 |
. . . . . 6
β’ (π β π΄ β V) |
18 | 15, 17 | eqeltrd 2834 |
. . . . 5
β’ (π β dom πΉ β V) |
19 | | rabexg 5292 |
. . . . 5
β’ (dom
πΉ β V β {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ} β V) |
20 | | mptexg 7175 |
. . . . 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 6975 |
. . 3
β’ (π β ( β³ βπΉ) = (π₯ β {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ} β¦ ((πΉβ(π₯ + 1)) β (πΉβπ₯)))) |
23 | 15 | eleq2d 2820 |
. . . . 5
β’ (π β ((π¦ + 1) β dom πΉ β (π¦ + 1) β π΄)) |
24 | 15, 23 | rabeqbidv 3423 |
. . . 4
β’ (π β {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ} = {π¦ β π΄ β£ (π¦ + 1) β π΄}) |
25 | 24 | mpteq1d 5204 |
. . 3
β’ (π β (π₯ β {π¦ β dom πΉ β£ (π¦ + 1) β dom πΉ} β¦ ((πΉβ(π₯ + 1)) β (πΉβπ₯))) = (π₯ β {π¦ β π΄ β£ (π¦ + 1) β π΄} β¦ ((πΉβ(π₯ + 1)) β (πΉβπ₯)))) |
26 | 22, 25 | eqtrd 2773 |
. 2
β’ (π β ( β³ βπΉ) = (π₯ β {π¦ β π΄ β£ (π¦ + 1) β π΄} β¦ ((πΉβ(π₯ + 1)) β (πΉβπ₯)))) |
27 | | fvoveq1 7384 |
. . . 4
β’ (π₯ = π β (πΉβ(π₯ + 1)) = (πΉβ(π + 1))) |
28 | | fveq2 6846 |
. . . 4
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
29 | 27, 28 | oveq12d 7379 |
. . 3
β’ (π₯ = π β ((πΉβ(π₯ + 1)) β (πΉβπ₯)) = ((πΉβ(π + 1)) β (πΉβπ))) |
30 | 29 | adantl 483 |
. 2
β’ ((π β§ π₯ = π) β ((πΉβ(π₯ + 1)) β (πΉβπ₯)) = ((πΉβ(π + 1)) β (πΉβπ))) |
31 | | fwddifval.3 |
. . 3
β’ (π β π β π΄) |
32 | | fwddifval.4 |
. . 3
β’ (π β (π + 1) β π΄) |
33 | | oveq1 7368 |
. . . . 5
β’ (π¦ = π β (π¦ + 1) = (π + 1)) |
34 | 33 | eleq1d 2819 |
. . . 4
β’ (π¦ = π β ((π¦ + 1) β π΄ β (π + 1) β π΄)) |
35 | 34 | elrab 3649 |
. . 3
β’ (π β {π¦ β π΄ β£ (π¦ + 1) β π΄} β (π β π΄ β§ (π + 1) β π΄)) |
36 | 31, 32, 35 | sylanbrc 584 |
. 2
β’ (π β π β {π¦ β π΄ β£ (π¦ + 1) β π΄}) |
37 | | ovexd 7396 |
. 2
β’ (π β ((πΉβ(π + 1)) β (πΉβπ)) β V) |
38 | 26, 30, 36, 37 | fvmptd 6959 |
1
β’ (π β (( β³ βπΉ)βπ) = ((πΉβ(π + 1)) β (πΉβπ))) |