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 | | fveq1 6841 |
. . . . . 6
β’ (π = 1 β (πβπ) = ( 1 βπ)) |
4 | | dchrsum.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
5 | | dchrsum.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
6 | | dchrsum.1 |
. . . . . . 7
β’ 1 =
(0gβπΊ) |
7 | | dchrsum2.u |
. . . . . . 7
β’ π = (Unitβπ) |
8 | | dchrsum.x |
. . . . . . . . 9
β’ (π β π β π·) |
9 | | dchrsum.d |
. . . . . . . . . 10
β’ π· = (BaseβπΊ) |
10 | 4, 9 | dchrrcl 26588 |
. . . . . . . . 9
β’ (π β π· β π β β) |
11 | 8, 10 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
12 | 11 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β π) β π β β) |
13 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π β π) β π β π) |
14 | 4, 5, 6, 7, 12, 13 | dchr1 26605 |
. . . . . 6
β’ ((π β§ π β π) β ( 1 βπ) = 1) |
15 | 3, 14 | sylan9eqr 2798 |
. . . . 5
β’ (((π β§ π β π) β§ π = 1 ) β (πβπ) = 1) |
16 | 15 | an32s 650 |
. . . 4
β’ (((π β§ π = 1 ) β§ π β π) β (πβπ) = 1) |
17 | 16 | sumeq2dv 15588 |
. . 3
β’ ((π β§ π = 1 ) β Ξ£π β π (πβπ) = Ξ£π β π 1) |
18 | 5, 7 | znunithash 20971 |
. . . . . . . . 9
β’ (π β β β
(β―βπ) =
(Οβπ)) |
19 | 11, 18 | syl 17 |
. . . . . . . 8
β’ (π β (β―βπ) = (Οβπ)) |
20 | 11 | phicld 16644 |
. . . . . . . . 9
β’ (π β (Οβπ) β
β) |
21 | 20 | nnnn0d 12473 |
. . . . . . . 8
β’ (π β (Οβπ) β
β0) |
22 | 19, 21 | eqeltrd 2837 |
. . . . . . 7
β’ (π β (β―βπ) β
β0) |
23 | 7 | fvexi 6856 |
. . . . . . . 8
β’ π β V |
24 | | hashclb 14258 |
. . . . . . . 8
β’ (π β V β (π β Fin β
(β―βπ) β
β0)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
β’ (π β Fin β
(β―βπ) β
β0) |
26 | 22, 25 | sylibr 233 |
. . . . . 6
β’ (π β π β Fin) |
27 | | ax-1cn 11109 |
. . . . . 6
β’ 1 β
β |
28 | | fsumconst 15675 |
. . . . . 6
β’ ((π β Fin β§ 1 β
β) β Ξ£π
β π 1 =
((β―βπ) Β·
1)) |
29 | 26, 27, 28 | sylancl 586 |
. . . . 5
β’ (π β Ξ£π β π 1 = ((β―βπ) Β· 1)) |
30 | 19 | oveq1d 7372 |
. . . . 5
β’ (π β ((β―βπ) Β· 1) =
((Οβπ) Β·
1)) |
31 | 20 | nncnd 12169 |
. . . . . 6
β’ (π β (Οβπ) β
β) |
32 | 31 | mulid1d 11172 |
. . . . 5
β’ (π β ((Οβπ) Β· 1) =
(Οβπ)) |
33 | 29, 30, 32 | 3eqtrd 2780 |
. . . 4
β’ (π β Ξ£π β π 1 = (Οβπ)) |
34 | 33 | adantr 481 |
. . 3
β’ ((π β§ π = 1 ) β Ξ£π β π 1 = (Οβπ)) |
35 | 17, 34 | eqtrd 2776 |
. 2
β’ ((π β§ π = 1 ) β Ξ£π β π (πβπ) = (Οβπ)) |
36 | 4 | dchrabl 26602 |
. . . . . . . 8
β’ (π β β β πΊ β Abel) |
37 | | ablgrp 19567 |
. . . . . . . 8
β’ (πΊ β Abel β πΊ β Grp) |
38 | 9, 6 | grpidcl 18778 |
. . . . . . . 8
β’ (πΊ β Grp β 1 β π·) |
39 | 11, 36, 37, 38 | 4syl 19 |
. . . . . . 7
β’ (π β 1 β π·) |
40 | 4, 5, 9, 7, 8, 39 | dchreq 26606 |
. . . . . 6
β’ (π β (π = 1 β βπ β π (πβπ) = ( 1 βπ))) |
41 | 40 | notbid 317 |
. . . . 5
β’ (π β (Β¬ π = 1 β Β¬ βπ β π (πβπ) = ( 1 βπ))) |
42 | | rexnal 3103 |
. . . . 5
β’
(βπ β
π Β¬ (πβπ) = ( 1 βπ) β Β¬ βπ β π (πβπ) = ( 1 βπ)) |
43 | 41, 42 | bitr4di 288 |
. . . 4
β’ (π β (Β¬ π = 1 β βπ β π Β¬ (πβπ) = ( 1 βπ))) |
44 | | df-ne 2944 |
. . . . . 6
β’ ((πβπ) β ( 1 βπ) β Β¬ (πβπ) = ( 1 βπ)) |
45 | 11 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β β) |
46 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
47 | 4, 5, 6, 7, 45, 46 | dchr1 26605 |
. . . . . . . 8
β’ ((π β§ π β π) β ( 1 βπ) = 1) |
48 | 47 | neeq2d 3004 |
. . . . . . 7
β’ ((π β§ π β π) β ((πβπ) β ( 1 βπ) β (πβπ) β 1)) |
49 | 26 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β Fin) |
50 | | eqid 2736 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
51 | 4, 5, 9, 50, 8 | dchrf 26590 |
. . . . . . . . . . . 12
β’ (π β π:(Baseβπ)βΆβ) |
52 | 50, 7 | unitss 20089 |
. . . . . . . . . . . . 13
β’ π β (Baseβπ) |
53 | 52 | sseli 3940 |
. . . . . . . . . . . 12
β’ (π β π β π β (Baseβπ)) |
54 | | ffvelcdm 7032 |
. . . . . . . . . . . 12
β’ ((π:(Baseβπ)βΆβ β§ π β (Baseβπ)) β (πβπ) β β) |
55 | 51, 53, 54 | syl2an 596 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πβπ) β β) |
56 | 55 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β (πβπ) β β) |
57 | 49, 56 | fsumcl 15618 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) β β) |
58 | | 0cnd 11148 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β 0 β
β) |
59 | 51 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π:(Baseβπ)βΆβ) |
60 | | simprl 769 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β π) |
61 | 52, 60 | sselid 3942 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β (Baseβπ)) |
62 | 59, 61 | ffvelcdmd 7036 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (πβπ) β β) |
63 | | subcl 11400 |
. . . . . . . . . 10
β’ (((πβπ) β β β§ 1 β β)
β ((πβπ) β 1) β
β) |
64 | 62, 27, 63 | sylancl 586 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) β 1) β β) |
65 | | simprr 771 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (πβπ) β 1) |
66 | | subeq0 11427 |
. . . . . . . . . . . 12
β’ (((πβπ) β β β§ 1 β β)
β (((πβπ) β 1) = 0 β (πβπ) = 1)) |
67 | 62, 27, 66 | sylancl 586 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) = 0 β (πβπ) = 1)) |
68 | 67 | necon3bid 2988 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) β 0 β (πβπ) β 1)) |
69 | 65, 68 | mpbird 256 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) β 1) β 0) |
70 | | oveq2 7365 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π(.rβπ)π₯) = (π(.rβπ)π)) |
71 | 70 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (πβ(π(.rβπ)π₯)) = (πβ(π(.rβπ)π))) |
72 | 71 | cbvsumv 15581 |
. . . . . . . . . . . . . 14
β’
Ξ£π₯ β
π (πβ(π(.rβπ)π₯)) = Ξ£π β π (πβ(π(.rβπ)π)) |
73 | 4, 5, 9 | dchrmhm 26589 |
. . . . . . . . . . . . . . . . . 18
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
74 | 73, 8 | sselid 3942 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
75 | 74 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
76 | 61 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β (Baseβπ)) |
77 | 53 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β (Baseβπ)) |
78 | | eqid 2736 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpβπ) =
(mulGrpβπ) |
79 | 78, 50 | mgpbas 19902 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
80 | | eqid 2736 |
. . . . . . . . . . . . . . . . . 18
β’
(.rβπ) = (.rβπ) |
81 | 78, 80 | mgpplusg 19900 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
82 | | eqid 2736 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpββfld) =
(mulGrpββfld) |
83 | | cnfldmul 20802 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββfld) |
84 | 82, 83 | mgpplusg 19900 |
. . . . . . . . . . . . . . . . 17
β’ Β·
= (+gβ(mulGrpββfld)) |
85 | 79, 81, 84 | mhmlin 18609 |
. . . . . . . . . . . . . . . 16
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π β (Baseβπ) β§ π β (Baseβπ)) β (πβ(π(.rβπ)π)) = ((πβπ) Β· (πβπ))) |
86 | 75, 76, 77, 85 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β (πβ(π(.rβπ)π)) = ((πβπ) Β· (πβπ))) |
87 | 86 | sumeq2dv 15588 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβ(π(.rβπ)π)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
88 | 72, 87 | eqtrid 2788 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π₯ β π (πβ(π(.rβπ)π₯)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
89 | | fveq2 6842 |
. . . . . . . . . . . . . 14
β’ (π = (π(.rβπ)π₯) β (πβπ) = (πβ(π(.rβπ)π₯))) |
90 | 11 | nnnn0d 12473 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
91 | 5 | zncrng 20951 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
CRing) |
92 | | crngring 19976 |
. . . . . . . . . . . . . . . 16
β’ (π β CRing β π β Ring) |
93 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’
((mulGrpβπ)
βΎs π) =
((mulGrpβπ)
βΎs π) |
94 | 7, 93 | unitgrp 20096 |
. . . . . . . . . . . . . . . 16
β’ (π β Ring β
((mulGrpβπ)
βΎs π)
β Grp) |
95 | 90, 91, 92, 94 | 4syl 19 |
. . . . . . . . . . . . . . 15
β’ (π β ((mulGrpβπ) βΎs π) β Grp) |
96 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
β’ (π β π β¦ (π β π β¦ (π(.rβπ)π))) = (π β π β¦ (π β π β¦ (π(.rβπ)π))) |
97 | 7, 93 | unitgrpbas 20095 |
. . . . . . . . . . . . . . . 16
β’ π =
(Baseβ((mulGrpβπ) βΎs π)) |
98 | 93, 81 | ressplusg 17171 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β
(.rβπ) =
(+gβ((mulGrpβπ) βΎs π))) |
99 | 23, 98 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(.rβπ) =
(+gβ((mulGrpβπ) βΎs π)) |
100 | 96, 97, 99 | grplactf1o 18851 |
. . . . . . . . . . . . . . 15
β’
((((mulGrpβπ)
βΎs π)
β Grp β§ π β
π) β ((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ):πβ1-1-ontoβπ) |
101 | 95, 60, 100 | syl2an2r 683 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ):πβ1-1-ontoβπ) |
102 | 96, 97 | grplactval 18849 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π₯ β π) β (((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ)βπ₯) = (π(.rβπ)π₯)) |
103 | 60, 102 | sylan 580 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π₯ β π) β (((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ)βπ₯) = (π(.rβπ)π₯)) |
104 | 89, 49, 101, 103, 56 | fsumf1o 15608 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) = Ξ£π₯ β π (πβ(π(.rβπ)π₯))) |
105 | 49, 62, 56 | fsummulc2 15669 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) Β· Ξ£π β π (πβπ)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
106 | 88, 104, 105 | 3eqtr4rd 2787 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) Β· Ξ£π β π (πβπ)) = Ξ£π β π (πβπ)) |
107 | 57 | mulid2d 11173 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (1 Β· Ξ£π β π (πβπ)) = Ξ£π β π (πβπ)) |
108 | 106, 107 | oveq12d 7375 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ))) = (Ξ£π β π (πβπ) β Ξ£π β π (πβπ))) |
109 | 57 | subidd 11500 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (Ξ£π β π (πβπ) β Ξ£π β π (πβπ)) = 0) |
110 | 108, 109 | eqtrd 2776 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ))) = 0) |
111 | | 1cnd 11150 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β 1 β
β) |
112 | 62, 111, 57 | subdird 11612 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· Ξ£π β π (πβπ)) = (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ)))) |
113 | 64 | mul01d 11354 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· 0) =
0) |
114 | 110, 112,
113 | 3eqtr4d 2786 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· Ξ£π β π (πβπ)) = (((πβπ) β 1) Β· 0)) |
115 | 57, 58, 64, 69, 114 | mulcanad 11790 |
. . . . . . . 8
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) = 0) |
116 | 115 | expr 457 |
. . . . . . 7
β’ ((π β§ π β π) β ((πβπ) β 1 β Ξ£π β π (πβπ) = 0)) |
117 | 48, 116 | sylbid 239 |
. . . . . 6
β’ ((π β§ π β π) β ((πβπ) β ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
118 | 44, 117 | biimtrrid 242 |
. . . . 5
β’ ((π β§ π β π) β (Β¬ (πβπ) = ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
119 | 118 | rexlimdva 3152 |
. . . 4
β’ (π β (βπ β π Β¬ (πβπ) = ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
120 | 43, 119 | sylbid 239 |
. . 3
β’ (π β (Β¬ π = 1 β Ξ£π β π (πβπ) = 0)) |
121 | 120 | imp 407 |
. 2
β’ ((π β§ Β¬ π = 1 ) β Ξ£π β π (πβπ) = 0) |
122 | 1, 2, 35, 121 | ifbothda 4524 |
1
β’ (π β Ξ£π β π (πβπ) = if(π = 1 , (Οβπ), 0)) |