Step | Hyp | Ref
| Expression |
1 | | eqeq2 2748 |
. 2
β’
((β―βπ·) =
if(π΄ = 1 , (β―βπ·), 0) β (Ξ£π₯ β π· (π₯βπ΄) = (β―βπ·) β Ξ£π₯ β π· (π₯βπ΄) = if(π΄ = 1 , (β―βπ·), 0))) |
2 | | eqeq2 2748 |
. 2
β’ (0 =
if(π΄ = 1 , (β―βπ·), 0) β (Ξ£π₯ β π· (π₯βπ΄) = 0 β Ξ£π₯ β π· (π₯βπ΄) = if(π΄ = 1 , (β―βπ·), 0))) |
3 | | fveq2 6842 |
. . . . . 6
β’ (π΄ = 1 β (π₯βπ΄) = (π₯β 1 )) |
4 | | sumdchr.g |
. . . . . . . . 9
β’ πΊ = (DChrβπ) |
5 | | sumdchr2.z |
. . . . . . . . 9
β’ π =
(β€/nβ€βπ) |
6 | | sumdchr.d |
. . . . . . . . 9
β’ π· = (BaseβπΊ) |
7 | 4, 5, 6 | dchrmhm 26589 |
. . . . . . . 8
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
8 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β π₯ β π·) |
9 | 7, 8 | sselid 3942 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
10 | | eqid 2736 |
. . . . . . . . 9
β’
(mulGrpβπ) =
(mulGrpβπ) |
11 | | sumdchr2.1 |
. . . . . . . . 9
β’ 1 =
(1rβπ) |
12 | 10, 11 | ringidval 19915 |
. . . . . . . 8
β’ 1 =
(0gβ(mulGrpβπ)) |
13 | | eqid 2736 |
. . . . . . . . 9
β’
(mulGrpββfld) =
(mulGrpββfld) |
14 | | cnfld1 20822 |
. . . . . . . . 9
β’ 1 =
(1rββfld) |
15 | 13, 14 | ringidval 19915 |
. . . . . . . 8
β’ 1 =
(0gβ(mulGrpββfld)) |
16 | 12, 15 | mhm0 18610 |
. . . . . . 7
β’ (π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (π₯β 1 ) = 1) |
17 | 9, 16 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (π₯β 1 ) = 1) |
18 | 3, 17 | sylan9eqr 2798 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ π΄ = 1 ) β (π₯βπ΄) = 1) |
19 | 18 | an32s 650 |
. . . 4
β’ (((π β§ π΄ = 1 ) β§ π₯ β π·) β (π₯βπ΄) = 1) |
20 | 19 | sumeq2dv 15588 |
. . 3
β’ ((π β§ π΄ = 1 ) β Ξ£π₯ β π· (π₯βπ΄) = Ξ£π₯ β π· 1) |
21 | | sumdchr2.n |
. . . . . . 7
β’ (π β π β β) |
22 | 4, 6 | dchrfi 26603 |
. . . . . . 7
β’ (π β β β π· β Fin) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ (π β π· β Fin) |
24 | | ax-1cn 11109 |
. . . . . 6
β’ 1 β
β |
25 | | fsumconst 15675 |
. . . . . 6
β’ ((π· β Fin β§ 1 β
β) β Ξ£π₯
β π· 1 =
((β―βπ·) Β·
1)) |
26 | 23, 24, 25 | sylancl 586 |
. . . . 5
β’ (π β Ξ£π₯ β π· 1 = ((β―βπ·) Β· 1)) |
27 | | hashcl 14256 |
. . . . . . . 8
β’ (π· β Fin β
(β―βπ·) β
β0) |
28 | 21, 22, 27 | 3syl 18 |
. . . . . . 7
β’ (π β (β―βπ·) β
β0) |
29 | 28 | nn0cnd 12475 |
. . . . . 6
β’ (π β (β―βπ·) β
β) |
30 | 29 | mulid1d 11172 |
. . . . 5
β’ (π β ((β―βπ·) Β· 1) =
(β―βπ·)) |
31 | 26, 30 | eqtrd 2776 |
. . . 4
β’ (π β Ξ£π₯ β π· 1 = (β―βπ·)) |
32 | 31 | adantr 481 |
. . 3
β’ ((π β§ π΄ = 1 ) β Ξ£π₯ β π· 1 = (β―βπ·)) |
33 | 20, 32 | eqtrd 2776 |
. 2
β’ ((π β§ π΄ = 1 ) β Ξ£π₯ β π· (π₯βπ΄) = (β―βπ·)) |
34 | | df-ne 2944 |
. . 3
β’ (π΄ β 1 β Β¬ π΄ = 1 ) |
35 | | sumdchr2.b |
. . . . 5
β’ π΅ = (Baseβπ) |
36 | 21 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β 1 ) β π β β) |
37 | | simpr 485 |
. . . . 5
β’ ((π β§ π΄ β 1 ) β π΄ β 1 ) |
38 | | sumdchr2.x |
. . . . . 6
β’ (π β π΄ β π΅) |
39 | 38 | adantr 481 |
. . . . 5
β’ ((π β§ π΄ β 1 ) β π΄ β π΅) |
40 | 4, 5, 6, 35, 11, 36, 37, 39 | dchrpt 26615 |
. . . 4
β’ ((π β§ π΄ β 1 ) β βπ¦ β π· (π¦βπ΄) β 1) |
41 | 36 | adantr 481 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β π β β) |
42 | 41, 22 | syl 17 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β π· β Fin) |
43 | | simpr 485 |
. . . . . . . 8
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π₯ β π·) |
44 | 4, 5, 6, 35, 43 | dchrf 26590 |
. . . . . . 7
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π₯:π΅βΆβ) |
45 | 39 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β π΄ β π΅) |
46 | 45 | adantr 481 |
. . . . . . 7
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π΄ β π΅) |
47 | 44, 46 | ffvelcdmd 7036 |
. . . . . 6
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β (π₯βπ΄) β β) |
48 | 42, 47 | fsumcl 15618 |
. . . . 5
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β Ξ£π₯ β π· (π₯βπ΄) β β) |
49 | | 0cnd 11148 |
. . . . 5
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β 0 β
β) |
50 | | simprl 769 |
. . . . . . . 8
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β π¦ β π·) |
51 | 4, 5, 6, 35, 50 | dchrf 26590 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β π¦:π΅βΆβ) |
52 | 51, 45 | ffvelcdmd 7036 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (π¦βπ΄) β β) |
53 | | subcl 11400 |
. . . . . 6
β’ (((π¦βπ΄) β β β§ 1 β β)
β ((π¦βπ΄) β 1) β
β) |
54 | 52, 24, 53 | sylancl 586 |
. . . . 5
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β ((π¦βπ΄) β 1) β
β) |
55 | | simprr 771 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (π¦βπ΄) β 1) |
56 | | subeq0 11427 |
. . . . . . . 8
β’ (((π¦βπ΄) β β β§ 1 β β)
β (((π¦βπ΄) β 1) = 0 β (π¦βπ΄) = 1)) |
57 | 52, 24, 56 | sylancl 586 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) β 1) = 0 β (π¦βπ΄) = 1)) |
58 | 57 | necon3bid 2988 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) β 1) β 0 β (π¦βπ΄) β 1)) |
59 | 55, 58 | mpbird 256 |
. . . . 5
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β ((π¦βπ΄) β 1) β 0) |
60 | | oveq2 7365 |
. . . . . . . . . . . 12
β’ (π§ = π₯ β (π¦(+gβπΊ)π§) = (π¦(+gβπΊ)π₯)) |
61 | 60 | fveq1d 6844 |
. . . . . . . . . . 11
β’ (π§ = π₯ β ((π¦(+gβπΊ)π§)βπ΄) = ((π¦(+gβπΊ)π₯)βπ΄)) |
62 | 61 | cbvsumv 15581 |
. . . . . . . . . 10
β’
Ξ£π§ β
π· ((π¦(+gβπΊ)π§)βπ΄) = Ξ£π₯ β π· ((π¦(+gβπΊ)π₯)βπ΄) |
63 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
64 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π¦ β π·) |
65 | 4, 5, 6, 63, 64, 43 | dchrmul 26596 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β (π¦(+gβπΊ)π₯) = (π¦ βf Β· π₯)) |
66 | 65 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β ((π¦(+gβπΊ)π₯)βπ΄) = ((π¦ βf Β· π₯)βπ΄)) |
67 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π¦:π΅βΆβ) |
68 | 67 | ffnd 6669 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π¦ Fn π΅) |
69 | 44 | ffnd 6669 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π₯ Fn π΅) |
70 | 35 | fvexi 6856 |
. . . . . . . . . . . . . 14
β’ π΅ β V |
71 | 70 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β π΅ β V) |
72 | | fnfvof 7634 |
. . . . . . . . . . . . 13
β’ (((π¦ Fn π΅ β§ π₯ Fn π΅) β§ (π΅ β V β§ π΄ β π΅)) β ((π¦ βf Β· π₯)βπ΄) = ((π¦βπ΄) Β· (π₯βπ΄))) |
73 | 68, 69, 71, 46, 72 | syl22anc 837 |
. . . . . . . . . . . 12
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β ((π¦ βf Β· π₯)βπ΄) = ((π¦βπ΄) Β· (π₯βπ΄))) |
74 | 66, 73 | eqtrd 2776 |
. . . . . . . . . . 11
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π₯ β π·) β ((π¦(+gβπΊ)π₯)βπ΄) = ((π¦βπ΄) Β· (π₯βπ΄))) |
75 | 74 | sumeq2dv 15588 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β Ξ£π₯ β π· ((π¦(+gβπΊ)π₯)βπ΄) = Ξ£π₯ β π· ((π¦βπ΄) Β· (π₯βπ΄))) |
76 | 62, 75 | eqtrid 2788 |
. . . . . . . . 9
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β Ξ£π§ β π· ((π¦(+gβπΊ)π§)βπ΄) = Ξ£π₯ β π· ((π¦βπ΄) Β· (π₯βπ΄))) |
77 | | fveq1 6841 |
. . . . . . . . . 10
β’ (π₯ = (π¦(+gβπΊ)π§) β (π₯βπ΄) = ((π¦(+gβπΊ)π§)βπ΄)) |
78 | 4 | dchrabl 26602 |
. . . . . . . . . . . 12
β’ (π β β β πΊ β Abel) |
79 | | ablgrp 19567 |
. . . . . . . . . . . 12
β’ (πΊ β Abel β πΊ β Grp) |
80 | 41, 78, 79 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β πΊ β Grp) |
81 | | eqid 2736 |
. . . . . . . . . . . 12
β’ (π β π· β¦ (π β π· β¦ (π(+gβπΊ)π))) = (π β π· β¦ (π β π· β¦ (π(+gβπΊ)π))) |
82 | 81, 6, 63 | grplactf1o 18851 |
. . . . . . . . . . 11
β’ ((πΊ β Grp β§ π¦ β π·) β ((π β π· β¦ (π β π· β¦ (π(+gβπΊ)π)))βπ¦):π·β1-1-ontoβπ·) |
83 | 80, 50, 82 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β ((π β π· β¦ (π β π· β¦ (π(+gβπΊ)π)))βπ¦):π·β1-1-ontoβπ·) |
84 | 81, 6 | grplactval 18849 |
. . . . . . . . . . 11
β’ ((π¦ β π· β§ π§ β π·) β (((π β π· β¦ (π β π· β¦ (π(+gβπΊ)π)))βπ¦)βπ§) = (π¦(+gβπΊ)π§)) |
85 | 50, 84 | sylan 580 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β§ π§ β π·) β (((π β π· β¦ (π β π· β¦ (π(+gβπΊ)π)))βπ¦)βπ§) = (π¦(+gβπΊ)π§)) |
86 | 77, 42, 83, 85, 47 | fsumf1o 15608 |
. . . . . . . . 9
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β Ξ£π₯ β π· (π₯βπ΄) = Ξ£π§ β π· ((π¦(+gβπΊ)π§)βπ΄)) |
87 | 42, 52, 47 | fsummulc2 15669 |
. . . . . . . . 9
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β ((π¦βπ΄) Β· Ξ£π₯ β π· (π₯βπ΄)) = Ξ£π₯ β π· ((π¦βπ΄) Β· (π₯βπ΄))) |
88 | 76, 86, 87 | 3eqtr4rd 2787 |
. . . . . . . 8
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β ((π¦βπ΄) Β· Ξ£π₯ β π· (π₯βπ΄)) = Ξ£π₯ β π· (π₯βπ΄)) |
89 | 48 | mulid2d 11173 |
. . . . . . . 8
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (1 Β· Ξ£π₯ β π· (π₯βπ΄)) = Ξ£π₯ β π· (π₯βπ΄)) |
90 | 88, 89 | oveq12d 7375 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) Β· Ξ£π₯ β π· (π₯βπ΄)) β (1 Β· Ξ£π₯ β π· (π₯βπ΄))) = (Ξ£π₯ β π· (π₯βπ΄) β Ξ£π₯ β π· (π₯βπ΄))) |
91 | 48 | subidd 11500 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (Ξ£π₯ β π· (π₯βπ΄) β Ξ£π₯ β π· (π₯βπ΄)) = 0) |
92 | 90, 91 | eqtrd 2776 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) Β· Ξ£π₯ β π· (π₯βπ΄)) β (1 Β· Ξ£π₯ β π· (π₯βπ΄))) = 0) |
93 | 24 | a1i 11 |
. . . . . . 7
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β 1 β
β) |
94 | 52, 93, 48 | subdird 11612 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) β 1) Β· Ξ£π₯ β π· (π₯βπ΄)) = (((π¦βπ΄) Β· Ξ£π₯ β π· (π₯βπ΄)) β (1 Β· Ξ£π₯ β π· (π₯βπ΄)))) |
95 | 54 | mul01d 11354 |
. . . . . 6
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) β 1) Β· 0) =
0) |
96 | 92, 94, 95 | 3eqtr4d 2786 |
. . . . 5
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β (((π¦βπ΄) β 1) Β· Ξ£π₯ β π· (π₯βπ΄)) = (((π¦βπ΄) β 1) Β· 0)) |
97 | 48, 49, 54, 59, 96 | mulcanad 11790 |
. . . 4
β’ (((π β§ π΄ β 1 ) β§ (π¦ β π· β§ (π¦βπ΄) β 1)) β Ξ£π₯ β π· (π₯βπ΄) = 0) |
98 | 40, 97 | rexlimddv 3158 |
. . 3
β’ ((π β§ π΄ β 1 ) β Ξ£π₯ β π· (π₯βπ΄) = 0) |
99 | 34, 98 | sylan2br 595 |
. 2
β’ ((π β§ Β¬ π΄ = 1 ) β Ξ£π₯ β π· (π₯βπ΄) = 0) |
100 | 1, 2, 33, 99 | ifbothda 4524 |
1
β’ (π β Ξ£π₯ β π· (π₯βπ΄) = if(π΄ = 1 , (β―βπ·), 0)) |