Step | Hyp | Ref
| Expression |
1 | | eqeq2 2745 |
. 2
β’
((Οβπ) =
if(π = 1 , (Οβπ), 0) β (Ξ£π β π (πβπ) = (Οβπ) β Ξ£π β π (πβπ) = if(π = 1 , (Οβπ), 0))) |
2 | | eqeq2 2745 |
. 2
β’ (0 =
if(π = 1 , (Οβπ), 0) β (Ξ£π β π (πβπ) = 0 β Ξ£π β π (πβπ) = if(π = 1 , (Οβπ), 0))) |
3 | | fveq1 6887 |
. . . . . 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 26723 |
. . . . . . . . 9
β’ (π β π· β π β β) |
11 | 8, 10 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β π β β) |
13 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β π) β π β π) |
14 | 4, 5, 6, 7, 12, 13 | dchr1 26740 |
. . . . . 6
β’ ((π β§ π β π) β ( 1 βπ) = 1) |
15 | 3, 14 | sylan9eqr 2795 |
. . . . 5
β’ (((π β§ π β π) β§ π = 1 ) β (πβπ) = 1) |
16 | 15 | an32s 651 |
. . . 4
β’ (((π β§ π = 1 ) β§ π β π) β (πβπ) = 1) |
17 | 16 | sumeq2dv 15645 |
. . 3
β’ ((π β§ π = 1 ) β Ξ£π β π (πβπ) = Ξ£π β π 1) |
18 | 5, 7 | znunithash 21104 |
. . . . . . . . 9
β’ (π β β β
(β―βπ) =
(Οβπ)) |
19 | 11, 18 | syl 17 |
. . . . . . . 8
β’ (π β (β―βπ) = (Οβπ)) |
20 | 11 | phicld 16701 |
. . . . . . . . 9
β’ (π β (Οβπ) β
β) |
21 | 20 | nnnn0d 12528 |
. . . . . . . 8
β’ (π β (Οβπ) β
β0) |
22 | 19, 21 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (β―βπ) β
β0) |
23 | 7 | fvexi 6902 |
. . . . . . . 8
β’ π β V |
24 | | hashclb 14314 |
. . . . . . . 8
β’ (π β V β (π β Fin β
(β―βπ) β
β0)) |
25 | 23, 24 | ax-mp 5 |
. . . . . . 7
β’ (π β Fin β
(β―βπ) β
β0) |
26 | 22, 25 | sylibr 233 |
. . . . . 6
β’ (π β π β Fin) |
27 | | ax-1cn 11164 |
. . . . . 6
β’ 1 β
β |
28 | | fsumconst 15732 |
. . . . . 6
β’ ((π β Fin β§ 1 β
β) β Ξ£π
β π 1 =
((β―βπ) Β·
1)) |
29 | 26, 27, 28 | sylancl 587 |
. . . . 5
β’ (π β Ξ£π β π 1 = ((β―βπ) Β· 1)) |
30 | 19 | oveq1d 7419 |
. . . . 5
β’ (π β ((β―βπ) Β· 1) =
((Οβπ) Β·
1)) |
31 | 20 | nncnd 12224 |
. . . . . 6
β’ (π β (Οβπ) β
β) |
32 | 31 | mulridd 11227 |
. . . . 5
β’ (π β ((Οβπ) Β· 1) =
(Οβπ)) |
33 | 29, 30, 32 | 3eqtrd 2777 |
. . . 4
β’ (π β Ξ£π β π 1 = (Οβπ)) |
34 | 33 | adantr 482 |
. . 3
β’ ((π β§ π = 1 ) β Ξ£π β π 1 = (Οβπ)) |
35 | 17, 34 | eqtrd 2773 |
. 2
β’ ((π β§ π = 1 ) β Ξ£π β π (πβπ) = (Οβπ)) |
36 | 4 | dchrabl 26737 |
. . . . . . . 8
β’ (π β β β πΊ β Abel) |
37 | | ablgrp 19646 |
. . . . . . . 8
β’ (πΊ β Abel β πΊ β Grp) |
38 | 9, 6 | grpidcl 18846 |
. . . . . . . 8
β’ (πΊ β Grp β 1 β π·) |
39 | 11, 36, 37, 38 | 4syl 19 |
. . . . . . 7
β’ (π β 1 β π·) |
40 | 4, 5, 9, 7, 8, 39 | dchreq 26741 |
. . . . . 6
β’ (π β (π = 1 β βπ β π (πβπ) = ( 1 βπ))) |
41 | 40 | notbid 318 |
. . . . 5
β’ (π β (Β¬ π = 1 β Β¬ βπ β π (πβπ) = ( 1 βπ))) |
42 | | rexnal 3101 |
. . . . 5
β’
(βπ β
π Β¬ (πβπ) = ( 1 βπ) β Β¬ βπ β π (πβπ) = ( 1 βπ)) |
43 | 41, 42 | bitr4di 289 |
. . . 4
β’ (π β (Β¬ π = 1 β βπ β π Β¬ (πβπ) = ( 1 βπ))) |
44 | | df-ne 2942 |
. . . . . 6
β’ ((πβπ) β ( 1 βπ) β Β¬ (πβπ) = ( 1 βπ)) |
45 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β β) |
46 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π) |
47 | 4, 5, 6, 7, 45, 46 | dchr1 26740 |
. . . . . . . 8
β’ ((π β§ π β π) β ( 1 βπ) = 1) |
48 | 47 | neeq2d 3002 |
. . . . . . 7
β’ ((π β§ π β π) β ((πβπ) β ( 1 βπ) β (πβπ) β 1)) |
49 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β Fin) |
50 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
51 | 4, 5, 9, 50, 8 | dchrf 26725 |
. . . . . . . . . . . 12
β’ (π β π:(Baseβπ)βΆβ) |
52 | 50, 7 | unitss 20179 |
. . . . . . . . . . . . 13
β’ π β (Baseβπ) |
53 | 52 | sseli 3977 |
. . . . . . . . . . . 12
β’ (π β π β π β (Baseβπ)) |
54 | | ffvelcdm 7079 |
. . . . . . . . . . . 12
β’ ((π:(Baseβπ)βΆβ β§ π β (Baseβπ)) β (πβπ) β β) |
55 | 51, 53, 54 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πβπ) β β) |
56 | 55 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β (πβπ) β β) |
57 | 49, 56 | fsumcl 15675 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) β β) |
58 | | 0cnd 11203 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β 0 β
β) |
59 | 51 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π:(Baseβπ)βΆβ) |
60 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β π) |
61 | 52, 60 | sselid 3979 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β π β (Baseβπ)) |
62 | 59, 61 | ffvelcdmd 7083 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (πβπ) β β) |
63 | | subcl 11455 |
. . . . . . . . . 10
β’ (((πβπ) β β β§ 1 β β)
β ((πβπ) β 1) β
β) |
64 | 62, 27, 63 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) β 1) β β) |
65 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (πβπ) β 1) |
66 | | subeq0 11482 |
. . . . . . . . . . . 12
β’ (((πβπ) β β β§ 1 β β)
β (((πβπ) β 1) = 0 β (πβπ) = 1)) |
67 | 62, 27, 66 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) = 0 β (πβπ) = 1)) |
68 | 67 | necon3bid 2986 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) β 0 β (πβπ) β 1)) |
69 | 65, 68 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) β 1) β 0) |
70 | | oveq2 7412 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π(.rβπ)π₯) = (π(.rβπ)π)) |
71 | 70 | fveq2d 6892 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (πβ(π(.rβπ)π₯)) = (πβ(π(.rβπ)π))) |
72 | 71 | cbvsumv 15638 |
. . . . . . . . . . . . . 14
β’
Ξ£π₯ β
π (πβ(π(.rβπ)π₯)) = Ξ£π β π (πβ(π(.rβπ)π)) |
73 | 4, 5, 9 | dchrmhm 26724 |
. . . . . . . . . . . . . . . . . 18
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
74 | 73, 8 | sselid 3979 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
75 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
76 | 61 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β (Baseβπ)) |
77 | 53 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β π β (Baseβπ)) |
78 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpβπ) =
(mulGrpβπ) |
79 | 78, 50 | mgpbas 19985 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
80 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(.rβπ) = (.rβπ) |
81 | 78, 80 | mgpplusg 19983 |
. . . . . . . . . . . . . . . . 17
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
82 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(mulGrpββfld) =
(mulGrpββfld) |
83 | | cnfldmul 20935 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββfld) |
84 | 82, 83 | mgpplusg 19983 |
. . . . . . . . . . . . . . . . 17
β’ Β·
= (+gβ(mulGrpββfld)) |
85 | 79, 81, 84 | mhmlin 18675 |
. . . . . . . . . . . . . . . 16
β’ ((π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π β (Baseβπ) β§ π β (Baseβπ)) β (πβ(π(.rβπ)π)) = ((πβπ) Β· (πβπ))) |
86 | 75, 76, 77, 85 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π β π) β (πβ(π(.rβπ)π)) = ((πβπ) Β· (πβπ))) |
87 | 86 | sumeq2dv 15645 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβ(π(.rβπ)π)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
88 | 72, 87 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π₯ β π (πβ(π(.rβπ)π₯)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
89 | | fveq2 6888 |
. . . . . . . . . . . . . 14
β’ (π = (π(.rβπ)π₯) β (πβπ) = (πβ(π(.rβπ)π₯))) |
90 | 11 | nnnn0d 12528 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
91 | 5 | zncrng 21084 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
CRing) |
92 | | crngring 20059 |
. . . . . . . . . . . . . . . 16
β’ (π β CRing β π β Ring) |
93 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
((mulGrpβπ)
βΎs π) =
((mulGrpβπ)
βΎs π) |
94 | 7, 93 | unitgrp 20186 |
. . . . . . . . . . . . . . . 16
β’ (π β Ring β
((mulGrpβπ)
βΎs π)
β Grp) |
95 | 90, 91, 92, 94 | 4syl 19 |
. . . . . . . . . . . . . . 15
β’ (π β ((mulGrpβπ) βΎs π) β Grp) |
96 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π β¦ (π β π β¦ (π(.rβπ)π))) = (π β π β¦ (π β π β¦ (π(.rβπ)π))) |
97 | 7, 93 | unitgrpbas 20185 |
. . . . . . . . . . . . . . . 16
β’ π =
(Baseβ((mulGrpβπ) βΎs π)) |
98 | 93, 81 | ressplusg 17231 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β
(.rβπ) =
(+gβ((mulGrpβπ) βΎs π))) |
99 | 23, 98 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(.rβπ) =
(+gβ((mulGrpβπ) βΎs π)) |
100 | 96, 97, 99 | grplactf1o 18923 |
. . . . . . . . . . . . . . 15
β’
((((mulGrpβπ)
βΎs π)
β Grp β§ π β
π) β ((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ):πβ1-1-ontoβπ) |
101 | 95, 60, 100 | syl2an2r 684 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ):πβ1-1-ontoβπ) |
102 | 96, 97 | grplactval 18921 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π₯ β π) β (((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ)βπ₯) = (π(.rβπ)π₯)) |
103 | 60, 102 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π β§ (πβπ) β 1)) β§ π₯ β π) β (((π β π β¦ (π β π β¦ (π(.rβπ)π)))βπ)βπ₯) = (π(.rβπ)π₯)) |
104 | 89, 49, 101, 103, 56 | fsumf1o 15665 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) = Ξ£π₯ β π (πβ(π(.rβπ)π₯))) |
105 | 49, 62, 56 | fsummulc2 15726 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) Β· Ξ£π β π (πβπ)) = Ξ£π β π ((πβπ) Β· (πβπ))) |
106 | 88, 104, 105 | 3eqtr4rd 2784 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β ((πβπ) Β· Ξ£π β π (πβπ)) = Ξ£π β π (πβπ)) |
107 | 57 | mullidd 11228 |
. . . . . . . . . . . 12
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (1 Β· Ξ£π β π (πβπ)) = Ξ£π β π (πβπ)) |
108 | 106, 107 | oveq12d 7422 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ))) = (Ξ£π β π (πβπ) β Ξ£π β π (πβπ))) |
109 | 57 | subidd 11555 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (Ξ£π β π (πβπ) β Ξ£π β π (πβπ)) = 0) |
110 | 108, 109 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ))) = 0) |
111 | | 1cnd 11205 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ (πβπ) β 1)) β 1 β
β) |
112 | 62, 111, 57 | subdird 11667 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· Ξ£π β π (πβπ)) = (((πβπ) Β· Ξ£π β π (πβπ)) β (1 Β· Ξ£π β π (πβπ)))) |
113 | 64 | mul01d 11409 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· 0) =
0) |
114 | 110, 112,
113 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ (πβπ) β 1)) β (((πβπ) β 1) Β· Ξ£π β π (πβπ)) = (((πβπ) β 1) Β· 0)) |
115 | 57, 58, 64, 69, 114 | mulcanad 11845 |
. . . . . . . 8
β’ ((π β§ (π β π β§ (πβπ) β 1)) β Ξ£π β π (πβπ) = 0) |
116 | 115 | expr 458 |
. . . . . . 7
β’ ((π β§ π β π) β ((πβπ) β 1 β Ξ£π β π (πβπ) = 0)) |
117 | 48, 116 | sylbid 239 |
. . . . . 6
β’ ((π β§ π β π) β ((πβπ) β ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
118 | 44, 117 | biimtrrid 242 |
. . . . 5
β’ ((π β§ π β π) β (Β¬ (πβπ) = ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
119 | 118 | rexlimdva 3156 |
. . . 4
β’ (π β (βπ β π Β¬ (πβπ) = ( 1 βπ) β Ξ£π β π (πβπ) = 0)) |
120 | 43, 119 | sylbid 239 |
. . 3
β’ (π β (Β¬ π = 1 β Ξ£π β π (πβπ) = 0)) |
121 | 120 | imp 408 |
. 2
β’ ((π β§ Β¬ π = 1 ) β Ξ£π β π (πβπ) = 0) |
122 | 1, 2, 35, 121 | ifbothda 4565 |
1
β’ (π β Ξ£π β π (πβπ) = if(π = 1 , (Οβπ), 0)) |