Step | Hyp | Ref
| Expression |
1 | | df-fwddifn 34775 |
. . . 4
β’
β³n = (π β β0, π β (β
βpm β) β¦ (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π)))))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β β³n =
(π β
β0, π
β (β βpm β) β¦ (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π))))))) |
3 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (0...π) = (0...π)) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β (0...π) = (0...π)) |
5 | | dmeq 5864 |
. . . . . . . . 9
β’ (π = πΉ β dom π = dom πΉ) |
6 | 5 | eleq2d 2824 |
. . . . . . . 8
β’ (π = πΉ β ((π¦ + π) β dom π β (π¦ + π) β dom πΉ)) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β ((π¦ + π) β dom π β (π¦ + π) β dom πΉ)) |
8 | 4, 7 | raleqbidv 3322 |
. . . . . 6
β’ ((π = π β§ π = πΉ) β (βπ β (0...π)(π¦ + π) β dom π β βπ β (0...π)(π¦ + π) β dom πΉ)) |
9 | 8 | rabbidv 3418 |
. . . . 5
β’ ((π = π β§ π = πΉ) β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} = {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ}) |
10 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (πCπ) = (πCπ)) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π = π β§ π = πΉ) β (πCπ) = (πCπ)) |
12 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = π β (π β π) = (π β π)) |
13 | 12 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π β (-1β(π β π)) = (-1β(π β π))) |
14 | | fveq1 6846 |
. . . . . . . . 9
β’ (π = πΉ β (πβ(π₯ + π)) = (πΉβ(π₯ + π))) |
15 | 13, 14 | oveqan12d 7381 |
. . . . . . . 8
β’ ((π = π β§ π = πΉ) β ((-1β(π β π)) Β· (πβ(π₯ + π))) = ((-1β(π β π)) Β· (πΉβ(π₯ + π)))) |
16 | 11, 15 | oveq12d 7380 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β ((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π)))) = ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π))))) |
17 | 16 | adantr 482 |
. . . . . 6
β’ (((π = π β§ π = πΉ) β§ π β (0...π)) β ((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π)))) = ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π))))) |
18 | 4, 17 | sumeq12dv 15598 |
. . . . 5
β’ ((π = π β§ π = πΉ) β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π))))) |
19 | 9, 18 | mpteq12dv 5201 |
. . . 4
β’ ((π = π β§ π = πΉ) β (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π))))) = (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))))) |
20 | 19 | adantl 483 |
. . 3
β’ ((π β§ (π = π β§ π = πΉ)) β (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom π} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πβ(π₯ + π))))) = (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))))) |
21 | | fwddifnval.1 |
. . 3
β’ (π β π β
β0) |
22 | | fwddifnval.3 |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
23 | | fwddifnval.2 |
. . . 4
β’ (π β π΄ β β) |
24 | | cnex 11139 |
. . . . 5
β’ β
β V |
25 | | elpm2r 8790 |
. . . . 5
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
26 | 24, 24, 25 | mpanl12 701 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
27 | 22, 23, 26 | syl2anc 585 |
. . 3
β’ (π β πΉ β (β βpm
β)) |
28 | 24 | mptrabex 7180 |
. . . 4
β’ (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π))))) β V |
29 | 28 | a1i 11 |
. . 3
β’ (π β (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π))))) β V) |
30 | 2, 20, 21, 27, 29 | ovmpod 7512 |
. 2
β’ (π β (π β³n πΉ) = (π₯ β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β¦ Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))))) |
31 | | fvoveq1 7385 |
. . . . . 6
β’ (π₯ = π β (πΉβ(π₯ + π)) = (πΉβ(π + π))) |
32 | 31 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π β ((-1β(π β π)) Β· (πΉβ(π₯ + π))) = ((-1β(π β π)) Β· (πΉβ(π + π)))) |
33 | 32 | oveq2d 7378 |
. . . 4
β’ (π₯ = π β ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))) = ((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
34 | 33 | sumeq2sdv 15596 |
. . 3
β’ (π₯ = π β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
35 | 34 | adantl 483 |
. 2
β’ ((π β§ π₯ = π) β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π₯ + π)))) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |
36 | | fwddifnval.4 |
. . 3
β’ (π β π β β) |
37 | | fwddifnval.5 |
. . . . 5
β’ ((π β§ π β (0...π)) β (π + π) β π΄) |
38 | 22 | fdmd 6684 |
. . . . . 6
β’ (π β dom πΉ = π΄) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...π)) β dom πΉ = π΄) |
40 | 37, 39 | eleqtrrd 2841 |
. . . 4
β’ ((π β§ π β (0...π)) β (π + π) β dom πΉ) |
41 | 40 | ralrimiva 3144 |
. . 3
β’ (π β βπ β (0...π)(π + π) β dom πΉ) |
42 | | oveq1 7369 |
. . . . . 6
β’ (π¦ = π β (π¦ + π) = (π + π)) |
43 | 42 | eleq1d 2823 |
. . . . 5
β’ (π¦ = π β ((π¦ + π) β dom πΉ β (π + π) β dom πΉ)) |
44 | 43 | ralbidv 3175 |
. . . 4
β’ (π¦ = π β (βπ β (0...π)(π¦ + π) β dom πΉ β βπ β (0...π)(π + π) β dom πΉ)) |
45 | 44 | elrab 3650 |
. . 3
β’ (π β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ} β (π β β β§ βπ β (0...π)(π + π) β dom πΉ)) |
46 | 36, 41, 45 | sylanbrc 584 |
. 2
β’ (π β π β {π¦ β β β£ βπ β (0...π)(π¦ + π) β dom πΉ}) |
47 | | sumex 15579 |
. . 3
β’
Ξ£π β
(0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) β V |
48 | 47 | a1i 11 |
. 2
β’ (π β Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π)))) β V) |
49 | 30, 35, 46, 48 | fvmptd 6960 |
1
β’ (π β ((π β³n πΉ)βπ) = Ξ£π β (0...π)((πCπ) Β· ((-1β(π β π)) Β· (πΉβ(π + π))))) |