Step | Hyp | Ref
| Expression |
1 | | isumclim3.3 |
. . 3
β’ (π β πΉ β dom β ) |
2 | | climdm 15442 |
. . 3
β’ (πΉ β dom β β πΉ β ( β βπΉ)) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π β πΉ β ( β βπΉ)) |
4 | | sumfc 15599 |
. . . 4
β’
Ξ£π β
π ((π β π β¦ π΄)βπ) = Ξ£π β π π΄ |
5 | | isumclim3.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
6 | | isumclim3.2 |
. . . . 5
β’ (π β π β β€) |
7 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
8 | | isumclim3.4 |
. . . . . . 7
β’ ((π β§ π β π) β π΄ β β) |
9 | 8 | fmpttd 7064 |
. . . . . 6
β’ (π β (π β π β¦ π΄):πβΆβ) |
10 | 9 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) β β) |
11 | 5, 6, 7, 10 | isum 15609 |
. . . 4
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = ( β βseqπ( + , (π β π β¦ π΄)))) |
12 | 4, 11 | eqtr3id 2787 |
. . 3
β’ (π β Ξ£π β π π΄ = ( β βseqπ( + , (π β π β¦ π΄)))) |
13 | | seqex 13914 |
. . . . . . 7
β’ seqπ( + , (π β π β¦ π΄)) β V |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β seqπ( + , (π β π β¦ π΄)) β V) |
15 | | isumclim3.5 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) = Ξ£π β (π...π)π΄) |
16 | | fvres 6862 |
. . . . . . . . . . 11
β’ (π β (π...π) β (((π β π β¦ π΄) βΎ (π...π))βπ) = ((π β π β¦ π΄)βπ)) |
17 | | fzssuz 13488 |
. . . . . . . . . . . . . 14
β’ (π...π) β (β€β₯βπ) |
18 | 17, 5 | sseqtrri 3982 |
. . . . . . . . . . . . 13
β’ (π...π) β π |
19 | | resmpt 5992 |
. . . . . . . . . . . . 13
β’ ((π...π) β π β ((π β π β¦ π΄) βΎ (π...π)) = (π β (π...π) β¦ π΄)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β π β¦ π΄) βΎ (π...π)) = (π β (π...π) β¦ π΄) |
21 | 20 | fveq1i 6844 |
. . . . . . . . . . 11
β’ (((π β π β¦ π΄) βΎ (π...π))βπ) = ((π β (π...π) β¦ π΄)βπ) |
22 | 16, 21 | eqtr3di 2788 |
. . . . . . . . . 10
β’ (π β (π...π) β ((π β π β¦ π΄)βπ) = ((π β (π...π) β¦ π΄)βπ)) |
23 | 22 | sumeq2i 15589 |
. . . . . . . . 9
β’
Ξ£π β
(π...π)((π β π β¦ π΄)βπ) = Ξ£π β (π...π)((π β (π...π) β¦ π΄)βπ) |
24 | | sumfc 15599 |
. . . . . . . . 9
β’
Ξ£π β
(π...π)((π β (π...π) β¦ π΄)βπ) = Ξ£π β (π...π)π΄ |
25 | 23, 24 | eqtri 2761 |
. . . . . . . 8
β’
Ξ£π β
(π...π)((π β π β¦ π΄)βπ) = Ξ£π β (π...π)π΄ |
26 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
27 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
28 | 27, 5 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
29 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π) |
30 | | elfzuz 13443 |
. . . . . . . . . . 11
β’ (π β (π...π) β π β (β€β₯βπ)) |
31 | 30, 5 | eleqtrrdi 2845 |
. . . . . . . . . 10
β’ (π β (π...π) β π β π) |
32 | 29, 31, 10 | syl2an 597 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ π΄)βπ) β β) |
33 | 26, 28, 32 | fsumser 15620 |
. . . . . . . 8
β’ ((π β§ π β π) β Ξ£π β (π...π)((π β π β¦ π΄)βπ) = (seqπ( + , (π β π β¦ π΄))βπ)) |
34 | 25, 33 | eqtr3id 2787 |
. . . . . . 7
β’ ((π β§ π β π) β Ξ£π β (π...π)π΄ = (seqπ( + , (π β π β¦ π΄))βπ)) |
35 | 15, 34 | eqtr2d 2774 |
. . . . . 6
β’ ((π β§ π β π) β (seqπ( + , (π β π β¦ π΄))βπ) = (πΉβπ)) |
36 | 5, 14, 1, 6, 35 | climeq 15455 |
. . . . 5
β’ (π β (seqπ( + , (π β π β¦ π΄)) β π₯ β πΉ β π₯)) |
37 | 36 | iotabidv 6481 |
. . . 4
β’ (π β (β©π₯seqπ( + , (π β π β¦ π΄)) β π₯) = (β©π₯πΉ β π₯)) |
38 | | df-fv 6505 |
. . . 4
β’ ( β
βseqπ( + , (π β π β¦ π΄))) = (β©π₯seqπ( + , (π β π β¦ π΄)) β π₯) |
39 | | df-fv 6505 |
. . . 4
β’ ( β
βπΉ) = (β©π₯πΉ β π₯) |
40 | 37, 38, 39 | 3eqtr4g 2798 |
. . 3
β’ (π β ( β βseqπ( + , (π β π β¦ π΄))) = ( β βπΉ)) |
41 | 12, 40 | eqtrd 2773 |
. 2
β’ (π β Ξ£π β π π΄ = ( β βπΉ)) |
42 | 3, 41 | breqtrrd 5134 |
1
β’ (π β πΉ β Ξ£π β π π΄) |