Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
β’
(β€/nβ€βπ) = (β€/nβ€βπ) |
2 | | eqid 2737 |
. . . . . 6
β’
(Baseβ(β€/nβ€βπ)) =
(Baseβ(β€/nβ€βπ)) |
3 | 1, 2 | znfi 20982 |
. . . . 5
β’ (π β β β
(Baseβ(β€/nβ€βπ)) β Fin) |
4 | | sumdchr.g |
. . . . . 6
β’ πΊ = (DChrβπ) |
5 | | sumdchr.d |
. . . . . 6
β’ π· = (BaseβπΊ) |
6 | 4, 5 | dchrfi 26619 |
. . . . 5
β’ (π β β β π· β Fin) |
7 | | simprr 772 |
. . . . . . 7
β’ ((π β β β§ (π β
(Baseβ(β€/nβ€βπ)) β§ π₯ β π·)) β π₯ β π·) |
8 | 4, 1, 5, 2, 7 | dchrf 26606 |
. . . . . 6
β’ ((π β β β§ (π β
(Baseβ(β€/nβ€βπ)) β§ π₯ β π·)) β π₯:(Baseβ(β€/nβ€βπ))βΆβ) |
9 | | simprl 770 |
. . . . . 6
β’ ((π β β β§ (π β
(Baseβ(β€/nβ€βπ)) β§ π₯ β π·)) β π β
(Baseβ(β€/nβ€βπ))) |
10 | 8, 9 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β β β§ (π β
(Baseβ(β€/nβ€βπ)) β§ π₯ β π·)) β (π₯βπ) β β) |
11 | 3, 6, 10 | fsumcom 15667 |
. . . 4
β’ (π β β β
Ξ£π β
(Baseβ(β€/nβ€βπ))Ξ£π₯ β π· (π₯βπ) = Ξ£π₯ β π· Ξ£π β
(Baseβ(β€/nβ€βπ))(π₯βπ)) |
12 | | eqid 2737 |
. . . . . . 7
β’
(1rβ(β€/nβ€βπ)) =
(1rβ(β€/nβ€βπ)) |
13 | | simpl 484 |
. . . . . . 7
β’ ((π β β β§ π β
(Baseβ(β€/nβ€βπ))) β π β β) |
14 | | simpr 486 |
. . . . . . 7
β’ ((π β β β§ π β
(Baseβ(β€/nβ€βπ))) β π β
(Baseβ(β€/nβ€βπ))) |
15 | 4, 5, 1, 12, 2, 13, 14 | sumdchr2 26634 |
. . . . . 6
β’ ((π β β β§ π β
(Baseβ(β€/nβ€βπ))) β Ξ£π₯ β π· (π₯βπ) = if(π =
(1rβ(β€/nβ€βπ)), (β―βπ·), 0)) |
16 | | velsn 4607 |
. . . . . . 7
β’ (π β
{(1rβ(β€/nβ€βπ))} β π =
(1rβ(β€/nβ€βπ))) |
17 | | ifbi 4513 |
. . . . . . 7
β’ ((π β
{(1rβ(β€/nβ€βπ))} β π =
(1rβ(β€/nβ€βπ))) β if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0) = if(π =
(1rβ(β€/nβ€βπ)), (β―βπ·), 0)) |
18 | 16, 17 | mp1i 13 |
. . . . . 6
β’ ((π β β β§ π β
(Baseβ(β€/nβ€βπ))) β if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0) = if(π =
(1rβ(β€/nβ€βπ)), (β―βπ·), 0)) |
19 | 15, 18 | eqtr4d 2780 |
. . . . 5
β’ ((π β β β§ π β
(Baseβ(β€/nβ€βπ))) β Ξ£π₯ β π· (π₯βπ) = if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0)) |
20 | 19 | sumeq2dv 15595 |
. . . 4
β’ (π β β β
Ξ£π β
(Baseβ(β€/nβ€βπ))Ξ£π₯ β π· (π₯βπ) = Ξ£π β
(Baseβ(β€/nβ€βπ))if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0)) |
21 | | eqid 2737 |
. . . . . . 7
β’
(0gβπΊ) = (0gβπΊ) |
22 | | simpr 486 |
. . . . . . 7
β’ ((π β β β§ π₯ β π·) β π₯ β π·) |
23 | 4, 1, 5, 21, 22, 2 | dchrsum 26633 |
. . . . . 6
β’ ((π β β β§ π₯ β π·) β Ξ£π β
(Baseβ(β€/nβ€βπ))(π₯βπ) = if(π₯ = (0gβπΊ), (Οβπ), 0)) |
24 | | velsn 4607 |
. . . . . . 7
β’ (π₯ β
{(0gβπΊ)}
β π₯ =
(0gβπΊ)) |
25 | | ifbi 4513 |
. . . . . . 7
β’ ((π₯ β
{(0gβπΊ)}
β π₯ =
(0gβπΊ))
β if(π₯ β
{(0gβπΊ)},
(Οβπ), 0) =
if(π₯ =
(0gβπΊ),
(Οβπ),
0)) |
26 | 24, 25 | mp1i 13 |
. . . . . 6
β’ ((π β β β§ π₯ β π·) β if(π₯ β {(0gβπΊ)}, (Οβπ), 0) = if(π₯ = (0gβπΊ), (Οβπ), 0)) |
27 | 23, 26 | eqtr4d 2780 |
. . . . 5
β’ ((π β β β§ π₯ β π·) β Ξ£π β
(Baseβ(β€/nβ€βπ))(π₯βπ) = if(π₯ β {(0gβπΊ)}, (Οβπ), 0)) |
28 | 27 | sumeq2dv 15595 |
. . . 4
β’ (π β β β
Ξ£π₯ β π· Ξ£π β
(Baseβ(β€/nβ€βπ))(π₯βπ) = Ξ£π₯ β π· if(π₯ β {(0gβπΊ)}, (Οβπ), 0)) |
29 | 11, 20, 28 | 3eqtr3d 2785 |
. . 3
β’ (π β β β
Ξ£π β
(Baseβ(β€/nβ€βπ))if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0) = Ξ£π₯ β π· if(π₯ β {(0gβπΊ)}, (Οβπ), 0)) |
30 | | nnnn0 12427 |
. . . . . 6
β’ (π β β β π β
β0) |
31 | 1 | zncrng 20967 |
. . . . . 6
β’ (π β β0
β (β€/nβ€βπ) β CRing) |
32 | | crngring 19983 |
. . . . . 6
β’
((β€/nβ€βπ) β CRing β
(β€/nβ€βπ) β Ring) |
33 | 2, 12 | ringidcl 19996 |
. . . . . 6
β’
((β€/nβ€βπ) β Ring β
(1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ))) |
34 | 30, 31, 32, 33 | 4syl 19 |
. . . . 5
β’ (π β β β
(1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ))) |
35 | 34 | snssd 4774 |
. . . 4
β’ (π β β β
{(1rβ(β€/nβ€βπ))} β
(Baseβ(β€/nβ€βπ))) |
36 | | hashcl 14263 |
. . . . . 6
β’ (π· β Fin β
(β―βπ·) β
β0) |
37 | | nn0cn 12430 |
. . . . . 6
β’
((β―βπ·)
β β0 β (β―βπ·) β β) |
38 | 6, 36, 37 | 3syl 18 |
. . . . 5
β’ (π β β β
(β―βπ·) β
β) |
39 | 38 | ralrimivw 3148 |
. . . 4
β’ (π β β β
βπ β
{(1rβ(β€/nβ€βπ))} (β―βπ·) β β) |
40 | 3 | olcd 873 |
. . . 4
β’ (π β β β
((Baseβ(β€/nβ€βπ)) β (β€β₯β0)
β¨ (Baseβ(β€/nβ€βπ)) β Fin)) |
41 | | sumss2 15618 |
. . . 4
β’
((({(1rβ(β€/nβ€βπ))} β
(Baseβ(β€/nβ€βπ)) β§ βπ β
{(1rβ(β€/nβ€βπ))} (β―βπ·) β β) β§
((Baseβ(β€/nβ€βπ)) β (β€β₯β0)
β¨ (Baseβ(β€/nβ€βπ)) β Fin)) β Ξ£π β
{(1rβ(β€/nβ€βπ))} (β―βπ·) = Ξ£π β
(Baseβ(β€/nβ€βπ))if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0)) |
42 | 35, 39, 40, 41 | syl21anc 837 |
. . 3
β’ (π β β β
Ξ£π β
{(1rβ(β€/nβ€βπ))} (β―βπ·) = Ξ£π β
(Baseβ(β€/nβ€βπ))if(π β
{(1rβ(β€/nβ€βπ))}, (β―βπ·), 0)) |
43 | 4 | dchrabl 26618 |
. . . . . 6
β’ (π β β β πΊ β Abel) |
44 | | ablgrp 19574 |
. . . . . 6
β’ (πΊ β Abel β πΊ β Grp) |
45 | 5, 21 | grpidcl 18785 |
. . . . . 6
β’ (πΊ β Grp β
(0gβπΊ)
β π·) |
46 | 43, 44, 45 | 3syl 18 |
. . . . 5
β’ (π β β β
(0gβπΊ)
β π·) |
47 | 46 | snssd 4774 |
. . . 4
β’ (π β β β
{(0gβπΊ)}
β π·) |
48 | | phicl 16648 |
. . . . . 6
β’ (π β β β
(Οβπ) β
β) |
49 | 48 | nncnd 12176 |
. . . . 5
β’ (π β β β
(Οβπ) β
β) |
50 | 49 | ralrimivw 3148 |
. . . 4
β’ (π β β β
βπ₯ β
{(0gβπΊ)}
(Οβπ) β
β) |
51 | 6 | olcd 873 |
. . . 4
β’ (π β β β (π· β
(β€β₯β0) β¨ π· β Fin)) |
52 | | sumss2 15618 |
. . . 4
β’
((({(0gβπΊ)} β π· β§ βπ₯ β {(0gβπΊ)} (Οβπ) β β) β§ (π· β
(β€β₯β0) β¨ π· β Fin)) β Ξ£π₯ β
{(0gβπΊ)}
(Οβπ) =
Ξ£π₯ β π· if(π₯ β {(0gβπΊ)}, (Οβπ), 0)) |
53 | 47, 50, 51, 52 | syl21anc 837 |
. . 3
β’ (π β β β
Ξ£π₯ β
{(0gβπΊ)}
(Οβπ) =
Ξ£π₯ β π· if(π₯ β {(0gβπΊ)}, (Οβπ), 0)) |
54 | 29, 42, 53 | 3eqtr4d 2787 |
. 2
β’ (π β β β
Ξ£π β
{(1rβ(β€/nβ€βπ))} (β―βπ·) = Ξ£π₯ β {(0gβπΊ)} (Οβπ)) |
55 | | eqidd 2738 |
. . . 4
β’ (π =
(1rβ(β€/nβ€βπ)) β (β―βπ·) = (β―βπ·)) |
56 | 55 | sumsn 15638 |
. . 3
β’
(((1rβ(β€/nβ€βπ)) β
(Baseβ(β€/nβ€βπ)) β§ (β―βπ·) β β) β Ξ£π β
{(1rβ(β€/nβ€βπ))} (β―βπ·) = (β―βπ·)) |
57 | 34, 38, 56 | syl2anc 585 |
. 2
β’ (π β β β
Ξ£π β
{(1rβ(β€/nβ€βπ))} (β―βπ·) = (β―βπ·)) |
58 | | eqidd 2738 |
. . . 4
β’ (π₯ = (0gβπΊ) β (Οβπ) = (Οβπ)) |
59 | 58 | sumsn 15638 |
. . 3
β’
(((0gβπΊ) β π· β§ (Οβπ) β β) β Ξ£π₯ β
{(0gβπΊ)}
(Οβπ) =
(Οβπ)) |
60 | 46, 49, 59 | syl2anc 585 |
. 2
β’ (π β β β
Ξ£π₯ β
{(0gβπΊ)}
(Οβπ) =
(Οβπ)) |
61 | 54, 57, 60 | 3eqtr3d 2785 |
1
β’ (π β β β
(β―βπ·) =
(Οβπ)) |