Step | Hyp | Ref
| Expression |
1 | | isumclim3.3 |
. . 3
β’ (π β πΉ β dom β ) |
2 | | climdm 15530 |
. . 3
β’ (πΉ β dom β β πΉ β ( β βπΉ)) |
3 | 1, 2 | sylib 217 |
. 2
β’ (π β πΉ β ( β βπΉ)) |
4 | | sumfc 15687 |
. . . 4
β’
Ξ£π β
π ((π β π β¦ π΄)βπ) = Ξ£π β π π΄ |
5 | | isumclim3.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
6 | | isumclim3.2 |
. . . . 5
β’ (π β π β β€) |
7 | | eqidd 2726 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
8 | | isumclim3.4 |
. . . . . . 7
β’ ((π β§ π β π) β π΄ β β) |
9 | 8 | fmpttd 7120 |
. . . . . 6
β’ (π β (π β π β¦ π΄):πβΆβ) |
10 | 9 | ffvelcdmda 7089 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) β β) |
11 | 5, 6, 7, 10 | isum 15697 |
. . . 4
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = ( β βseqπ( + , (π β π β¦ π΄)))) |
12 | 4, 11 | eqtr3id 2779 |
. . 3
β’ (π β Ξ£π β π π΄ = ( β βseqπ( + , (π β π β¦ π΄)))) |
13 | | seqex 14000 |
. . . . . . 7
β’ seqπ( + , (π β π β¦ π΄)) β V |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β seqπ( + , (π β π β¦ π΄)) β V) |
15 | | isumclim3.5 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) = Ξ£π β (π...π)π΄) |
16 | | fvres 6911 |
. . . . . . . . . . 11
β’ (π β (π...π) β (((π β π β¦ π΄) βΎ (π...π))βπ) = ((π β π β¦ π΄)βπ)) |
17 | | fzssuz 13574 |
. . . . . . . . . . . . . 14
β’ (π...π) β (β€β₯βπ) |
18 | 17, 5 | sseqtrri 4010 |
. . . . . . . . . . . . 13
β’ (π...π) β π |
19 | | resmpt 6036 |
. . . . . . . . . . . . 13
β’ ((π...π) β π β ((π β π β¦ π΄) βΎ (π...π)) = (π β (π...π) β¦ π΄)) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β π β¦ π΄) βΎ (π...π)) = (π β (π...π) β¦ π΄) |
21 | 20 | fveq1i 6893 |
. . . . . . . . . . 11
β’ (((π β π β¦ π΄) βΎ (π...π))βπ) = ((π β (π...π) β¦ π΄)βπ) |
22 | 16, 21 | eqtr3di 2780 |
. . . . . . . . . 10
β’ (π β (π...π) β ((π β π β¦ π΄)βπ) = ((π β (π...π) β¦ π΄)βπ)) |
23 | 22 | sumeq2i 15677 |
. . . . . . . . 9
β’
Ξ£π β
(π...π)((π β π β¦ π΄)βπ) = Ξ£π β (π...π)((π β (π...π) β¦ π΄)βπ) |
24 | | sumfc 15687 |
. . . . . . . . 9
β’
Ξ£π β
(π...π)((π β (π...π) β¦ π΄)βπ) = Ξ£π β (π...π)π΄ |
25 | 23, 24 | eqtri 2753 |
. . . . . . . 8
β’
Ξ£π β
(π...π)((π β π β¦ π΄)βπ) = Ξ£π β (π...π)π΄ |
26 | | eqidd 2726 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
27 | | simpr 483 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
28 | 27, 5 | eleqtrdi 2835 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
29 | | simpl 481 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π) |
30 | | elfzuz 13529 |
. . . . . . . . . . 11
β’ (π β (π...π) β π β (β€β₯βπ)) |
31 | 30, 5 | eleqtrrdi 2836 |
. . . . . . . . . 10
β’ (π β (π...π) β π β π) |
32 | 29, 31, 10 | syl2an 594 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (π...π)) β ((π β π β¦ π΄)βπ) β β) |
33 | 26, 28, 32 | fsumser 15708 |
. . . . . . . 8
β’ ((π β§ π β π) β Ξ£π β (π...π)((π β π β¦ π΄)βπ) = (seqπ( + , (π β π β¦ π΄))βπ)) |
34 | 25, 33 | eqtr3id 2779 |
. . . . . . 7
β’ ((π β§ π β π) β Ξ£π β (π...π)π΄ = (seqπ( + , (π β π β¦ π΄))βπ)) |
35 | 15, 34 | eqtr2d 2766 |
. . . . . 6
β’ ((π β§ π β π) β (seqπ( + , (π β π β¦ π΄))βπ) = (πΉβπ)) |
36 | 5, 14, 1, 6, 35 | climeq 15543 |
. . . . 5
β’ (π β (seqπ( + , (π β π β¦ π΄)) β π₯ β πΉ β π₯)) |
37 | 36 | iotabidv 6527 |
. . . 4
β’ (π β (β©π₯seqπ( + , (π β π β¦ π΄)) β π₯) = (β©π₯πΉ β π₯)) |
38 | | df-fv 6551 |
. . . 4
β’ ( β
βseqπ( + , (π β π β¦ π΄))) = (β©π₯seqπ( + , (π β π β¦ π΄)) β π₯) |
39 | | df-fv 6551 |
. . . 4
β’ ( β
βπΉ) = (β©π₯πΉ β π₯) |
40 | 37, 38, 39 | 3eqtr4g 2790 |
. . 3
β’ (π β ( β βseqπ( + , (π β π β¦ π΄))) = ( β βπΉ)) |
41 | 12, 40 | eqtrd 2765 |
. 2
β’ (π β Ξ£π β π π΄ = ( β βπΉ)) |
42 | 3, 41 | breqtrrd 5171 |
1
β’ (π β πΉ β Ξ£π β π π΄) |