Step | Hyp | Ref
| Expression |
1 | | sum0 11398 |
. . . 4
β’
Ξ£π β
β
π΅ =
0 |
2 | | fsumf1o.3 |
. . . . . . . 8
β’ (π β πΉ:πΆβ1-1-ontoβπ΄) |
3 | | f1oeq2 5452 |
. . . . . . . 8
β’ (πΆ = β
β (πΉ:πΆβ1-1-ontoβπ΄ β πΉ:β
β1-1-ontoβπ΄)) |
4 | 2, 3 | syl5ibcom 155 |
. . . . . . 7
β’ (π β (πΆ = β
β πΉ:β
β1-1-ontoβπ΄)) |
5 | 4 | imp 124 |
. . . . . 6
β’ ((π β§ πΆ = β
) β πΉ:β
β1-1-ontoβπ΄) |
6 | | f1ofo 5470 |
. . . . . 6
β’ (πΉ:β
β1-1-ontoβπ΄ β πΉ:β
βontoβπ΄) |
7 | | fo00 5499 |
. . . . . . 7
β’ (πΉ:β
βontoβπ΄ β (πΉ = β
β§ π΄ = β
)) |
8 | 7 | simprbi 275 |
. . . . . 6
β’ (πΉ:β
βontoβπ΄ β π΄ = β
) |
9 | 5, 6, 8 | 3syl 17 |
. . . . 5
β’ ((π β§ πΆ = β
) β π΄ = β
) |
10 | 9 | sumeq1d 11376 |
. . . 4
β’ ((π β§ πΆ = β
) β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
11 | | simpr 110 |
. . . . . 6
β’ ((π β§ πΆ = β
) β πΆ = β
) |
12 | 11 | sumeq1d 11376 |
. . . . 5
β’ ((π β§ πΆ = β
) β Ξ£π β πΆ π· = Ξ£π β β
π·) |
13 | | sum0 11398 |
. . . . 5
β’
Ξ£π β
β
π· =
0 |
14 | 12, 13 | eqtrdi 2226 |
. . . 4
β’ ((π β§ πΆ = β
) β Ξ£π β πΆ π· = 0) |
15 | 1, 10, 14 | 3eqtr4a 2236 |
. . 3
β’ ((π β§ πΆ = β
) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |
16 | 15 | ex 115 |
. 2
β’ (π β (πΆ = β
β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
17 | | 2fveq3 5522 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
18 | | simprl 529 |
. . . . . . . 8
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (β―βπΆ) β
β) |
19 | | simprr 531 |
. . . . . . . 8
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β π:(1...(β―βπΆ))β1-1-ontoβπΆ) |
20 | | f1of 5463 |
. . . . . . . . . . . 12
β’ (πΉ:πΆβ1-1-ontoβπ΄ β πΉ:πΆβΆπ΄) |
21 | 2, 20 | syl 14 |
. . . . . . . . . . 11
β’ (π β πΉ:πΆβΆπ΄) |
22 | 21 | ffvelcdmda 5653 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β (πΉβπ) β π΄) |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
24 | 23 | fmpttd 5673 |
. . . . . . . . . . 11
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
25 | 24 | ffvelcdmda 5653 |
. . . . . . . . . 10
β’ ((π β§ (πΉβπ) β π΄) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
26 | 22, 25 | syldan 282 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
27 | 26 | adantlr 477 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) β β) |
28 | 2 | adantr 276 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β πΉ:πΆβ1-1-ontoβπ΄) |
29 | | f1oco 5486 |
. . . . . . . . . . . 12
β’ ((πΉ:πΆβ1-1-ontoβπ΄ β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ) β (πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄) |
30 | 28, 19, 29 | syl2anc 411 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄) |
31 | | f1of 5463 |
. . . . . . . . . . 11
β’ ((πΉ β π):(1...(β―βπΆ))β1-1-ontoβπ΄ β (πΉ β π):(1...(β―βπΆ))βΆπ΄) |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (πΉ β π):(1...(β―βπΆ))βΆπ΄) |
33 | | fvco3 5589 |
. . . . . . . . . 10
β’ (((πΉ β π):(1...(β―βπΆ))βΆπ΄ β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
34 | 32, 33 | sylan 283 |
. . . . . . . . 9
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
35 | | f1of 5463 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπΆ))β1-1-ontoβπΆ β π:(1...(β―βπΆ))βΆπΆ) |
36 | 35 | ad2antll 491 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β π:(1...(β―βπΆ))βΆπΆ) |
37 | | fvco3 5589 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπΆ))βΆπΆ β§ π β (1...(β―βπΆ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
38 | 36, 37 | sylan 283 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
39 | 38 | fveq2d 5521 |
. . . . . . . . 9
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β ((π β π΄ β¦ π΅)β((πΉ β π)βπ)) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
40 | 34, 39 | eqtrd 2210 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β (1...(β―βπΆ))) β (((π β π΄ β¦ π΅) β (πΉ β π))βπ) = ((π β π΄ β¦ π΅)β(πΉβ(πβπ)))) |
41 | 17, 18, 19, 27, 40 | fsum3 11397 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β πΆ ((π β π΄ β¦ π΅)β(πΉβπ)) = (seq1( + , (π β β β¦ if(π β€ (β―βπΆ), (((π β π΄ β¦ π΅) β (πΉ β π))βπ), 0)))β(β―βπΆ))) |
42 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
43 | | fsumf1o.1 |
. . . . . . . . . . . . 13
β’ (π = πΊ β π΅ = π·) |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) |
45 | 21 | ffvelcdmda 5653 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β (πΉβπ) β π΄) |
46 | 44, 45 | eqeltrrd 2255 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β πΊ β π΄) |
47 | 43 | eleq1d 2246 |
. . . . . . . . . . . . . 14
β’ (π = πΊ β (π΅ β β β π· β β)) |
48 | 23 | ralrimiva 2550 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β π΄ π΅ β β) |
49 | 48 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΆ) β βπ β π΄ π΅ β β) |
50 | 47, 49, 46 | rspcdva 2848 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β π· β β) |
51 | 42, 43, 46, 50 | fvmptd3 5611 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)βπΊ) = π·) |
52 | 44 | fveq2d 5521 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)βπΊ)) |
53 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΆ) β π β πΆ) |
54 | | eqid 2177 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β¦ π·) = (π β πΆ β¦ π·) |
55 | 54 | fvmpt2 5601 |
. . . . . . . . . . . . 13
β’ ((π β πΆ β§ π· β β) β ((π β πΆ β¦ π·)βπ) = π·) |
56 | 53, 50, 55 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = π·) |
57 | 51, 52, 56 | 3eqtr4rd 2221 |
. . . . . . . . . . 11
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
58 | 57 | ralrimiva 2550 |
. . . . . . . . . 10
β’ (π β βπ β πΆ ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
59 | | nffvmpt1 5528 |
. . . . . . . . . . . 12
β’
β²π((π β πΆ β¦ π·)βπ) |
60 | 59 | nfeq1 2329 |
. . . . . . . . . . 11
β’
β²π((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) |
61 | | fveq2 5517 |
. . . . . . . . . . . 12
β’ (π = π β ((π β πΆ β¦ π·)βπ) = ((π β πΆ β¦ π·)βπ)) |
62 | | 2fveq3 5522 |
. . . . . . . . . . . 12
β’ (π = π β ((π β π΄ β¦ π΅)β(πΉβπ)) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
63 | 61, 62 | eqeq12d 2192 |
. . . . . . . . . . 11
β’ (π = π β (((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)))) |
64 | 60, 63 | rspc 2837 |
. . . . . . . . . 10
β’ (π β πΆ β (βπ β πΆ ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ)))) |
65 | 58, 64 | mpan9 281 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
66 | 65 | adantlr 477 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β πΆ) β ((π β πΆ β¦ π·)βπ) = ((π β π΄ β¦ π΅)β(πΉβπ))) |
67 | 66 | sumeq2dv 11378 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ ((π β π΄ β¦ π΅)β(πΉβπ))) |
68 | | fveq2 5517 |
. . . . . . . 8
β’ (π = ((πΉ β π)βπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β((πΉ β π)βπ))) |
69 | 24 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β (π β π΄ β¦ π΅):π΄βΆβ) |
70 | 69 | ffvelcdmda 5653 |
. . . . . . . 8
β’ (((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
71 | 68, 18, 30, 70, 34 | fsum3 11397 |
. . . . . . 7
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , (π β β β¦ if(π β€ (β―βπΆ), (((π β π΄ β¦ π΅) β (πΉ β π))βπ), 0)))β(β―βπΆ))) |
72 | 41, 67, 71 | 3eqtr4rd 2221 |
. . . . . 6
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β πΆ ((π β πΆ β¦ π·)βπ)) |
73 | | sumfct 11384 |
. . . . . . . 8
β’
(βπ β
π΄ π΅ β β β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅) |
74 | 48, 73 | syl 14 |
. . . . . . 7
β’ (π β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅) |
75 | 74 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅) |
76 | 50 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ β πΆ π· β β) |
77 | | sumfct 11384 |
. . . . . . . 8
β’
(βπ β
πΆ π· β β β Ξ£π β πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ π·) |
78 | 76, 77 | syl 14 |
. . . . . . 7
β’ (π β Ξ£π β πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ π·) |
79 | 78 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β πΆ ((π β πΆ β¦ π·)βπ) = Ξ£π β πΆ π·) |
80 | 72, 75, 79 | 3eqtr3d 2218 |
. . . . 5
β’ ((π β§ ((β―βπΆ) β β β§ π:(1...(β―βπΆ))β1-1-ontoβπΆ)) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |
81 | 80 | expr 375 |
. . . 4
β’ ((π β§ (β―βπΆ) β β) β (π:(1...(β―βπΆ))β1-1-ontoβπΆ β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
82 | 81 | exlimdv 1819 |
. . 3
β’ ((π β§ (β―βπΆ) β β) β
(βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
83 | 82 | expimpd 363 |
. 2
β’ (π β (((β―βπΆ) β β β§
βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ) β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·)) |
84 | | fsumf1o.2 |
. . 3
β’ (π β πΆ β Fin) |
85 | | fz1f1o 11385 |
. . 3
β’ (πΆ β Fin β (πΆ = β
β¨
((β―βπΆ) β
β β§ βπ
π:(1...(β―βπΆ))β1-1-ontoβπΆ))) |
86 | 84, 85 | syl 14 |
. 2
β’ (π β (πΆ = β
β¨ ((β―βπΆ) β β β§
βπ π:(1...(β―βπΆ))β1-1-ontoβπΆ))) |
87 | 16, 83, 86 | mpjaod 718 |
1
β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) |