Step | Hyp | Ref
| Expression |
1 | | muinv.1 |
. . 3
β’ (π β πΉ:ββΆβ) |
2 | 1 | feqmptd 6915 |
. 2
β’ (π β πΉ = (π β β β¦ (πΉβπ))) |
3 | | muinv.2 |
. . . . . . . . . 10
β’ (π β πΊ = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ))) |
4 | 3 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β πΊ = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ))) |
5 | 4 | fveq1d 6849 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (πΊβ(π / π)) = ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ))β(π / π))) |
6 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
7 | 6 | elrab 3650 |
. . . . . . . . . . . . 13
β’ (π β {π₯ β β β£ π₯ β₯ π} β (π β β β§ π β₯ π)) |
8 | 7 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β₯ π) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β₯ π) |
10 | | elrabi 3644 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β β) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
12 | 11 | nnzd 12533 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β€) |
13 | 11 | nnne0d 12210 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β 0) |
14 | | nnz 12527 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β€) |
16 | | dvdsval2 16146 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β 0 β§ π β β€) β (π β₯ π β (π / π) β β€)) |
17 | 12, 13, 15, 16 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π β₯ π β (π / π) β β€)) |
18 | 9, 17 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β€) |
19 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
20 | | nngt0 12191 |
. . . . . . . . . . . . 13
β’ (π β β β 0 <
π) |
21 | 19, 20 | jca 513 |
. . . . . . . . . . . 12
β’ (π β β β (π β β β§ 0 <
π)) |
22 | 21 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π β β β§ 0 < π)) |
23 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
24 | | nngt0 12191 |
. . . . . . . . . . . . 13
β’ (π β β β 0 <
π) |
25 | 23, 24 | jca 513 |
. . . . . . . . . . . 12
β’ (π β β β (π β β β§ 0 <
π)) |
26 | 11, 25 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π β β β§ 0 < π)) |
27 | | divgt0 12030 |
. . . . . . . . . . 11
β’ (((π β β β§ 0 <
π) β§ (π β β β§ 0 <
π)) β 0 < (π / π)) |
28 | 22, 26, 27 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β 0 < (π / π)) |
29 | | elnnz 12516 |
. . . . . . . . . 10
β’ ((π / π) β β β ((π / π) β β€ β§ 0 < (π / π))) |
30 | 18, 28, 29 | sylanbrc 584 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β) |
31 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = (π / π) β (π₯ β₯ π β π₯ β₯ (π / π))) |
32 | 31 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = (π / π) β {π₯ β β β£ π₯ β₯ π} = {π₯ β β β£ π₯ β₯ (π / π)}) |
33 | 32 | sumeq1d 15593 |
. . . . . . . . . 10
β’ (π = (π / π) β Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ)) |
34 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β β¦
Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ)) = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ)) |
35 | | sumex 15579 |
. . . . . . . . . 10
β’
Ξ£π β
{π₯ β β β£
π₯ β₯ (π / π)} (πΉβπ) β V |
36 | 33, 34, 35 | fvmpt 6953 |
. . . . . . . . 9
β’ ((π / π) β β β ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ))β(π / π)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ)) |
37 | 30, 36 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} (πΉβπ))β(π / π)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ)) |
38 | 5, 37 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (πΊβ(π / π)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ)) |
39 | 38 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· (πΊβ(π / π))) = ((ΞΌβπ) Β· Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ))) |
40 | | fzfid 13885 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (1...(π / π)) β Fin) |
41 | | dvdsssfz1 16207 |
. . . . . . . . 9
β’ ((π / π) β β β {π₯ β β β£ π₯ β₯ (π / π)} β (1...(π / π))) |
42 | 30, 41 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π)} β (1...(π / π))) |
43 | 40, 42 | ssfid 9218 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π)} β Fin) |
44 | | mucl 26506 |
. . . . . . . . 9
β’ (π β β β
(ΞΌβπ) β
β€) |
45 | 11, 44 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (ΞΌβπ) β β€) |
46 | 45 | zcnd 12615 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (ΞΌβπ) β β) |
47 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β πΉ:ββΆβ) |
48 | | elrabi 3644 |
. . . . . . . 8
β’ (π β {π₯ β β β£ π₯ β₯ (π / π)} β π β β) |
49 | | ffvelcdm 7037 |
. . . . . . . 8
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
50 | 47, 48, 49 | syl2an 597 |
. . . . . . 7
β’ ((((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π)}) β (πΉβπ) β β) |
51 | 43, 46, 50 | fsummulc2 15676 |
. . . . . 6
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (πΉβπ)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ))) |
52 | 39, 51 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((ΞΌβπ) Β· (πΊβ(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ))) |
53 | 52 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (πΊβ(π / π))) = Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ))) |
54 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
55 | 46 | adantrr 716 |
. . . . . 6
β’ (((π β§ π β β) β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π β {π₯ β β β£ π₯ β₯ (π / π)})) β (ΞΌβπ) β β) |
56 | 50 | anasss 468 |
. . . . . 6
β’ (((π β§ π β β) β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π β {π₯ β β β£ π₯ β₯ (π / π)})) β (πΉβπ) β β) |
57 | 55, 56 | mulcld 11182 |
. . . . 5
β’ (((π β§ π β β) β§ (π β {π₯ β β β£ π₯ β₯ π} β§ π β {π₯ β β β£ π₯ β₯ (π / π)})) β ((ΞΌβπ) Β· (πΉβπ)) β β) |
58 | 54, 57 | fsumdvdsdiag 26549 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ)) = Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ))) |
59 | | ssrab2 4042 |
. . . . . . . . . 10
β’ {π₯ β β β£ π₯ β₯ π} β β |
60 | | dvdsdivcl 16205 |
. . . . . . . . . . 11
β’ ((π β β β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β {π₯ β β β£ π₯ β₯ π}) |
61 | 60 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β {π₯ β β β£ π₯ β₯ π}) |
62 | 59, 61 | sselid 3947 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π / π) β β) |
63 | | musum 26556 |
. . . . . . . . 9
β’ ((π / π) β β β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (ΞΌβπ) = if((π / π) = 1, 1, 0)) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (ΞΌβπ) = if((π / π) = 1, 1, 0)) |
65 | 64 | oveq1d 7377 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (ΞΌβπ) Β· (πΉβπ)) = (if((π / π) = 1, 1, 0) Β· (πΉβπ))) |
66 | | fzfid 13885 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (1...(π / π)) β Fin) |
67 | | dvdsssfz1 16207 |
. . . . . . . . . 10
β’ ((π / π) β β β {π₯ β β β£ π₯ β₯ (π / π)} β (1...(π / π))) |
68 | 62, 67 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π)} β (1...(π / π))) |
69 | 66, 68 | ssfid 9218 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β {π₯ β β β£ π₯ β₯ (π / π)} β Fin) |
70 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ:ββΆβ) |
71 | | elrabi 3644 |
. . . . . . . . 9
β’ (π β {π₯ β β β£ π₯ β₯ π} β π β β) |
72 | 70, 71, 49 | syl2an 597 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (πΉβπ) β β) |
73 | | ssrab2 4042 |
. . . . . . . . . . 11
β’ {π₯ β β β£ π₯ β₯ (π / π)} β β |
74 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π)}) β π β {π₯ β β β£ π₯ β₯ (π / π)}) |
75 | 73, 74 | sselid 3947 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π)}) β π β β) |
76 | 75, 44 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π)}) β (ΞΌβπ) β β€) |
77 | 76 | zcnd 12615 |
. . . . . . . 8
β’ ((((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β§ π β {π₯ β β β£ π₯ β₯ (π / π)}) β (ΞΌβπ) β β) |
78 | 69, 72, 77 | fsummulc1 15677 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} (ΞΌβπ) Β· (πΉβπ)) = Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ))) |
79 | | ovif 7459 |
. . . . . . . 8
β’
(if((π / π) = 1, 1, 0) Β· (πΉβπ)) = if((π / π) = 1, (1 Β· (πΉβπ)), (0 Β· (πΉβπ))) |
80 | | nncn 12168 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
81 | 80 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
82 | 71 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
83 | 82 | nncnd 12176 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β β) |
84 | | 1cnd 11157 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β 1 β β) |
85 | 82 | nnne0d 12210 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β π β 0) |
86 | 81, 83, 84, 85 | divmuld 11960 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π / π) = 1 β (π Β· 1) = π)) |
87 | 83 | mulid1d 11179 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (π Β· 1) = π) |
88 | 87 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π Β· 1) = π β π = π)) |
89 | 86, 88 | bitrd 279 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β ((π / π) = 1 β π = π)) |
90 | 72 | mulid2d 11180 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (1 Β· (πΉβπ)) = (πΉβπ)) |
91 | 72 | mul02d 11360 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (0 Β· (πΉβπ)) = 0) |
92 | 89, 90, 91 | ifbieq12d 4519 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β if((π / π) = 1, (1 Β· (πΉβπ)), (0 Β· (πΉβπ))) = if(π = π, (πΉβπ), 0)) |
93 | 79, 92 | eqtrid 2789 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β (if((π / π) = 1, 1, 0) Β· (πΉβπ)) = if(π = π, (πΉβπ), 0)) |
94 | 65, 78, 93 | 3eqtr3d 2785 |
. . . . . 6
β’ (((π β§ π β β) β§ π β {π₯ β β β£ π₯ β₯ π}) β Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ)) = if(π = π, (πΉβπ), 0)) |
95 | 94 | sumeq2dv 15595 |
. . . . 5
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ)) = Ξ£π β {π₯ β β β£ π₯ β₯ π}if(π = π, (πΉβπ), 0)) |
96 | | breq1 5113 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β₯ π β π β₯ π)) |
97 | 54 | nnzd 12533 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β€) |
98 | | iddvds 16159 |
. . . . . . . . 9
β’ (π β β€ β π β₯ π) |
99 | 97, 98 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β π β₯ π) |
100 | 96, 54, 99 | elrabd 3652 |
. . . . . . 7
β’ ((π β§ π β β) β π β {π₯ β β β£ π₯ β₯ π}) |
101 | 100 | snssd 4774 |
. . . . . 6
β’ ((π β§ π β β) β {π} β {π₯ β β β£ π₯ β₯ π}) |
102 | 101 | sselda 3949 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β {π}) β π β {π₯ β β β£ π₯ β₯ π}) |
103 | 102, 72 | syldan 592 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β {π}) β (πΉβπ) β β) |
104 | | 0cn 11154 |
. . . . . . 7
β’ 0 β
β |
105 | | ifcl 4536 |
. . . . . . 7
β’ (((πΉβπ) β β β§ 0 β β)
β if(π = π, (πΉβπ), 0) β β) |
106 | 103, 104,
105 | sylancl 587 |
. . . . . 6
β’ (((π β§ π β β) β§ π β {π}) β if(π = π, (πΉβπ), 0) β β) |
107 | | eldifsni 4755 |
. . . . . . . . 9
β’ (π β ({π₯ β β β£ π₯ β₯ π} β {π}) β π β π) |
108 | 107 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β ({π₯ β β β£ π₯ β₯ π} β {π})) β π β π) |
109 | 108 | neneqd 2949 |
. . . . . . 7
β’ (((π β§ π β β) β§ π β ({π₯ β β β£ π₯ β₯ π} β {π})) β Β¬ π = π) |
110 | 109 | iffalsed 4502 |
. . . . . 6
β’ (((π β§ π β β) β§ π β ({π₯ β β β£ π₯ β₯ π} β {π})) β if(π = π, (πΉβπ), 0) = 0) |
111 | | fzfid 13885 |
. . . . . . 7
β’ ((π β§ π β β) β (1...π) β Fin) |
112 | | dvdsssfz1 16207 |
. . . . . . . 8
β’ (π β β β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
113 | 112 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β {π₯ β β β£ π₯ β₯ π} β (1...π)) |
114 | 111, 113 | ssfid 9218 |
. . . . . 6
β’ ((π β§ π β β) β {π₯ β β β£ π₯ β₯ π} β Fin) |
115 | 101, 106,
110, 114 | fsumss 15617 |
. . . . 5
β’ ((π β§ π β β) β Ξ£π β {π}if(π = π, (πΉβπ), 0) = Ξ£π β {π₯ β β β£ π₯ β₯ π}if(π = π, (πΉβπ), 0)) |
116 | 1 | ffvelcdmda 7040 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) β β) |
117 | | iftrue 4497 |
. . . . . . . 8
β’ (π = π β if(π = π, (πΉβπ), 0) = (πΉβπ)) |
118 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
119 | 117, 118 | eqtrd 2777 |
. . . . . . 7
β’ (π = π β if(π = π, (πΉβπ), 0) = (πΉβπ)) |
120 | 119 | sumsn 15638 |
. . . . . 6
β’ ((π β β β§ (πΉβπ) β β) β Ξ£π β {π}if(π = π, (πΉβπ), 0) = (πΉβπ)) |
121 | 54, 116, 120 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β β) β Ξ£π β {π}if(π = π, (πΉβπ), 0) = (πΉβπ)) |
122 | 95, 115, 121 | 3eqtr2d 2783 |
. . . 4
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π}Ξ£π β {π₯ β β β£ π₯ β₯ (π / π)} ((ΞΌβπ) Β· (πΉβπ)) = (πΉβπ)) |
123 | 53, 58, 122 | 3eqtrd 2781 |
. . 3
β’ ((π β§ π β β) β Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (πΊβ(π / π))) = (πΉβπ)) |
124 | 123 | mpteq2dva 5210 |
. 2
β’ (π β (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (πΊβ(π / π)))) = (π β β β¦ (πΉβπ))) |
125 | 2, 124 | eqtr4d 2780 |
1
β’ (π β πΉ = (π β β β¦ Ξ£π β {π₯ β β β£ π₯ β₯ π} ((ΞΌβπ) Β· (πΊβ(π / π))))) |