Step | Hyp | Ref
| Expression |
1 | | sum0 15607 |
. . . 4
β’
Ξ£π β
β
π΅ =
0 |
2 | | fsumf1o.3 |
. . . . . . . 8
β’ (π β πΉ:πΆβ1-1-ontoβπ΄) |
3 | | f1oeq2 6774 |
. . . . . . . 8
β’ (πΆ = β
β (πΉ:πΆβ1-1-ontoβπ΄ β πΉ:β
β1-1-ontoβπ΄)) |
4 | 2, 3 | syl5ibcom 244 |
. . . . . . 7
β’ (π β (πΆ = β
β πΉ:β
β1-1-ontoβπ΄)) |
5 | 4 | imp 408 |
. . . . . 6
β’ ((π β§ πΆ = β
) β πΉ:β
β1-1-ontoβπ΄) |
6 | | f1ofo 6792 |
. . . . . 6
β’ (πΉ:β
β1-1-ontoβπ΄ β πΉ:β
βontoβπ΄) |
7 | | fo00 6821 |
. . . . . . 7
β’ (πΉ:β
βontoβπ΄ β (πΉ = β
β§ π΄ = β
)) |
8 | 7 | simprbi 498 |
. . . . . 6
β’ (πΉ:β
βontoβπ΄ β π΄ = β
) |
9 | 5, 6, 8 | 3syl 18 |
. . . . 5
β’ ((π β§ πΆ = β
) β π΄ = β
) |
10 | 9 | sumeq1d 15587 |
. . . 4
β’ ((π β§ πΆ = β
) β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
11 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΆ = β
) β πΆ = β
) |
12 | 11 | sumeq1d 15587 |
. . . . 5
β’ ((π β§ πΆ = β
) β Ξ£π β πΆ π· = Ξ£π β β
π·) |
13 | | sum0 15607 |
. . . . 5
β’
Ξ£π β
β
π· =
0 |
14 | 12, 13 | eqtrdi 2793 |
. . . 4
β’ ((π β§ πΆ = β
) β Ξ£π β πΆ π· = 0) |
15 | 1, 10, 14 | 3eqtr4a 2803 |
. . 3
β’ ((π β§ πΆ = β
) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |
16 | 15 | ex 414 |
. 2
β’ (π β (πΆ = β
β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
17 | | 2fveq3 6848 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
18 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (β―βπΆ) β
β) |
19 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β π:(1...(β―βπΆ))β1-1-ontoβπΆ) |
20 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (πΉ:πΆβ1-1-ontoβπ΄ β πΉ:πΆβΆπ΄) |
21 | 2, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ:πΆβΆπ΄) |
22 | 21 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β (πΉβπ) β π΄) |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
24 | 23 | fmpttd 7064 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
25 | 24 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((π β§ (πΉβπ) β π΄) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
26 | 22, 25 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
27 | 26 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
28 | | f1oco 6808 |
. . . . . . . . . . . 12
β’ ((πΉ:πΆβ1-1-ontoβπ΄ β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ) β (πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄) |
29 | 2, 19, 28 | syl2an2r 684 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄) |
30 | | f1of 6785 |
. . . . . . . . . . 11
β’ ((πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄ β (πΉ β π):(1...(β―βπΆ))βΆπ΄) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (πΉ β π):(1...(β―βπΆ))βΆπ΄) |
32 | | fvco3 6941 |
. . . . . . . . . 10
β’ (((πΉ β π):(1...(β―βπΆ))βΆπ΄ β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
33 | 31, 32 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
34 | | f1of 6785 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπΆ))β1-1-ontoβπΆ β π:(1...(β―βπΆ))βΆπΆ) |
35 | 34 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β π:(1...(β―βπΆ))βΆπΆ) |
36 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπΆ))βΆπΆ β§ π β (1...(β―βπΆ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
37 | 35, 36 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
38 | 37 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β ((π β π΄ β¦ π΅)β((πΉ β π)βπ)) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
39 | 33, 38 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
40 | 17, 18, 19, 27, 39 | fsum 15606 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β πΆ ((π β π΄ β¦ π΅)β(πΉβπ)) = (seq1( + , ((π β π΄ β¦ π΅) β (πΉ β π)))β(β―βπΆ))) |
41 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) |
42 | 21 | ffvelcdmda 7036 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (πΉβπ) β π΄) |
43 | 41, 42 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β πΊ β π΄) |
44 | | fsumf1o.1 |
. . . . . . . . . . . . . 14
β’ (π = πΊ β π΅ = π·) |
45 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
46 | 44, 45 | fvmpti 6948 |
. . . . . . . . . . . . 13
β’ (πΊ β π΄ β ((π β π΄ β¦ π΅)βπΊ) = ( I βπ·)) |
47 | 43, 46 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)βπΊ) = ( I βπ·)) |
48 | 41 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)βπΊ)) |
49 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β¦ π·) = (π β πΆ β¦ π·) |
50 | 49 | fvmpt2i 6959 |
. . . . . . . . . . . . 13
β’ (π β πΆ β ((π β πΆ β¦ π·)βπ) = ( I βπ·)) |
51 | 50 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ( I βπ·)) |
52 | 47, 48, 51 | 3eqtr4rd 2788 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
53 | 52 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ β πΆ ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
54 | | nffvmpt1 6854 |
. . . . . . . . . . . 12
β’
β²π((π β πΆ β¦ π·)βπ) |
55 | 54 | nfeq1 2923 |
. . . . . . . . . . 11
β’
β²π((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) |
56 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β ((π β πΆ β¦ π·)βπ) = ((π β πΆ β¦ π·)βπ)) |
57 | | 2fveq3 6848 |
. . . . . . . . . . . 12
β’ (π = π β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
58 | 56, 57 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π = π β (((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)))) |
59 | 55, 58 | rspc 3570 |
. . . . . . . . . 10
β’ (π β πΆ β (βπ β πΆ ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)))) |
60 | 53, 59 | mpan9 508 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
61 | 60 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
62 | 61 | sumeq2dv 15589 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ ((π β π΄ β¦ π΅)β(πΉβπ))) |
63 | | fveq2 6843 |
. . . . . . . 8
β’ (π = ((πΉ β π)βπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
64 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (π β π΄ β¦ π΅):π΄βΆβ) |
65 | 64 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
66 | 63, 18, 29, 65, 33 | fsum 15606 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , ((π β π΄ β¦ π΅) β (πΉ β π)))β(β―βπΆ))) |
67 | 40, 62, 66 | 3eqtr4rd 2788 |
. . . . . 6
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β πΆ ((π β πΆ β¦ π·)βπ)) |
68 | | sumfc 15595 |
. . . . . 6
β’
Ξ£π β
π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅ |
69 | | sumfc 15595 |
. . . . . 6
β’
Ξ£π β
πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ π· |
70 | 67, 68, 69 | 3eqtr3g 2800 |
. . . . 5
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |
71 | 70 | expr 458 |
. . . 4
β’ ((π β§ (β―βπΆ) β β) β (π:(1...(β―βπΆ))β1-1-ontoβπΆ β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
72 | 71 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπΆ) β β) β
(βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
73 | 72 | expimpd 455 |
. 2
β’ (π β (((β―βπΆ) β β β§
βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
74 | | fsumf1o.2 |
. . 3
β’ (π β πΆ β Fin) |
75 | | fz1f1o 15596 |
. . 3
β’ (πΆ β Fin β (πΆ = β
β¨
((β―βπΆ) β
β β§ βπ
π:(1...(β―βπΆ))β1-1-ontoβπΆ))) |
76 | 74, 75 | syl 17 |
. 2
β’ (π β (πΆ = β
β¨ ((β―βπΆ) β β β§
βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ))) |
77 | 16, 73, 76 | mpjaod 859 |
1
β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |