Step | Hyp | Ref
| Expression |
1 | | dchrpt.g |
. . 3
β’ πΊ = (DChrβπ) |
2 | | dchrpt.z |
. . 3
β’ π =
(β€/nβ€βπ) |
3 | | dchrpt.b |
. . 3
β’ π΅ = (Baseβπ) |
4 | | dchrpt.u |
. . 3
β’ π = (Unitβπ) |
5 | | dchrpt.n |
. . 3
β’ (π β π β β) |
6 | | dchrpt.d |
. . 3
β’ π· = (BaseβπΊ) |
7 | | fveq2 6889 |
. . 3
β’ (π£ = π₯ β (πβπ£) = (πβπ₯)) |
8 | | fveq2 6889 |
. . 3
β’ (π£ = π¦ β (πβπ£) = (πβπ¦)) |
9 | | fveq2 6889 |
. . 3
β’ (π£ = (π₯(.rβπ)π¦) β (πβπ£) = (πβ(π₯(.rβπ)π¦))) |
10 | | fveq2 6889 |
. . 3
β’ (π£ = (1rβπ) β (πβπ£) = (πβ(1rβπ))) |
11 | | dchrpt.2 |
. . . . . . . . 9
β’ (π β π»dom DProd π) |
12 | | zex 12564 |
. . . . . . . . . . . . 13
β’ β€
β V |
13 | 12 | mptex 7222 |
. . . . . . . . . . . 12
β’ (π β β€ β¦ (π Β· (πβπ))) β V |
14 | 13 | rnex 7900 |
. . . . . . . . . . 11
β’ ran
(π β β€ β¦
(π Β· (πβπ))) β V |
15 | | dchrpt.s |
. . . . . . . . . . 11
β’ π = (π β dom π β¦ ran (π β β€ β¦ (π Β· (πβπ)))) |
16 | 14, 15 | dmmpti 6692 |
. . . . . . . . . 10
β’ dom π = dom π |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ (π β dom π = dom π) |
18 | | dchrpt.p |
. . . . . . . . 9
β’ π = (π»dProjπ) |
19 | | dchrpt.i |
. . . . . . . . 9
β’ (π β πΌ β dom π) |
20 | 11, 17, 18, 19 | dpjf 19922 |
. . . . . . . 8
β’ (π β (πβπΌ):(π» DProd π)βΆ(πβπΌ)) |
21 | | dchrpt.3 |
. . . . . . . . 9
β’ (π β (π» DProd π) = π) |
22 | 21 | feq2d 6701 |
. . . . . . . 8
β’ (π β ((πβπΌ):(π» DProd π)βΆ(πβπΌ) β (πβπΌ):πβΆ(πβπΌ))) |
23 | 20, 22 | mpbid 231 |
. . . . . . 7
β’ (π β (πβπΌ):πβΆ(πβπΌ)) |
24 | 23 | ffvelcdmda 7084 |
. . . . . 6
β’ ((π β§ π£ β π) β ((πβπΌ)βπ£) β (πβπΌ)) |
25 | 19 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β π) β πΌ β dom π) |
26 | | oveq1 7413 |
. . . . . . . . . . 11
β’ (π = π β (π Β· (πβπ)) = (π Β· (πβπ))) |
27 | 26 | cbvmptv 5261 |
. . . . . . . . . 10
β’ (π β β€ β¦ (π Β· (πβπ))) = (π β β€ β¦ (π Β· (πβπ))) |
28 | | fveq2 6889 |
. . . . . . . . . . . 12
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
29 | 28 | oveq2d 7422 |
. . . . . . . . . . 11
β’ (π = πΌ β (π Β· (πβπ)) = (π Β· (πβπΌ))) |
30 | 29 | mpteq2dv 5250 |
. . . . . . . . . 10
β’ (π = πΌ β (π β β€ β¦ (π Β· (πβπ))) = (π β β€ β¦ (π Β· (πβπΌ)))) |
31 | 27, 30 | eqtrid 2785 |
. . . . . . . . 9
β’ (π = πΌ β (π β β€ β¦ (π Β· (πβπ))) = (π β β€ β¦ (π Β· (πβπΌ)))) |
32 | 31 | rneqd 5936 |
. . . . . . . 8
β’ (π = πΌ β ran (π β β€ β¦ (π Β· (πβπ))) = ran (π β β€ β¦ (π Β· (πβπΌ)))) |
33 | 32, 15, 14 | fvmpt3i 7001 |
. . . . . . 7
β’ (πΌ β dom π β (πβπΌ) = ran (π β β€ β¦ (π Β· (πβπΌ)))) |
34 | 25, 33 | syl 17 |
. . . . . 6
β’ ((π β§ π£ β π) β (πβπΌ) = ran (π β β€ β¦ (π Β· (πβπΌ)))) |
35 | 24, 34 | eleqtrd 2836 |
. . . . 5
β’ ((π β§ π£ β π) β ((πβπΌ)βπ£) β ran (π β β€ β¦ (π Β· (πβπΌ)))) |
36 | | eqid 2733 |
. . . . . 6
β’ (π β β€ β¦ (π Β· (πβπΌ))) = (π β β€ β¦ (π Β· (πβπΌ))) |
37 | | ovex 7439 |
. . . . . 6
β’ (π Β· (πβπΌ)) β V |
38 | 36, 37 | elrnmpti 5958 |
. . . . 5
β’ (((πβπΌ)βπ£) β ran (π β β€ β¦ (π Β· (πβπΌ))) β βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ))) |
39 | 35, 38 | sylib 217 |
. . . 4
β’ ((π β§ π£ β π) β βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ))) |
40 | | dchrpt.1 |
. . . . . 6
β’ 1 =
(1rβπ) |
41 | | dchrpt.n1 |
. . . . . 6
β’ (π β π΄ β 1 ) |
42 | | dchrpt.h |
. . . . . 6
β’ π» = ((mulGrpβπ) βΎs π) |
43 | | dchrpt.m |
. . . . . 6
β’ Β· =
(.gβπ») |
44 | | dchrpt.au |
. . . . . 6
β’ (π β π΄ β π) |
45 | | dchrpt.w |
. . . . . 6
β’ (π β π β Word π) |
46 | | dchrpt.o |
. . . . . 6
β’ π = (odβπ») |
47 | | dchrpt.t |
. . . . . 6
β’ π =
(-1βπ(2 / (πβ(πβπΌ)))) |
48 | | dchrpt.4 |
. . . . . 6
β’ (π β ((πβπΌ)βπ΄) β 1 ) |
49 | | dchrpt.5 |
. . . . . 6
β’ π = (π’ β π β¦ (β©ββπ β β€ (((πβπΌ)βπ’) = (π Β· (πβπΌ)) β§ β = (πβπ)))) |
50 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . 5
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β (πβπ£) = (πβπ)) |
51 | | neg1cn 12323 |
. . . . . . . . 9
β’ -1 β
β |
52 | | 2re 12283 |
. . . . . . . . . . 11
β’ 2 β
β |
53 | 5 | nnnn0d 12529 |
. . . . . . . . . . . . . 14
β’ (π β π β
β0) |
54 | 2 | zncrng 21092 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
CRing) |
55 | | crngring 20062 |
. . . . . . . . . . . . . 14
β’ (π β CRing β π β Ring) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β π β Ring) |
57 | 4, 42 | unitgrp 20190 |
. . . . . . . . . . . . 13
β’ (π β Ring β π» β Grp) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π» β Grp) |
59 | 2, 3 | znfi 21107 |
. . . . . . . . . . . . . 14
β’ (π β β β π΅ β Fin) |
60 | 5, 59 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π΅ β Fin) |
61 | 3, 4 | unitss 20183 |
. . . . . . . . . . . . 13
β’ π β π΅ |
62 | | ssfi 9170 |
. . . . . . . . . . . . 13
β’ ((π΅ β Fin β§ π β π΅) β π β Fin) |
63 | 60, 61, 62 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β π β Fin) |
64 | | wrdf 14466 |
. . . . . . . . . . . . . 14
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
65 | 45, 64 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π:(0..^(β―βπ))βΆπ) |
66 | 65 | fdmd 6726 |
. . . . . . . . . . . . . 14
β’ (π β dom π = (0..^(β―βπ))) |
67 | 19, 66 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (π β πΌ β (0..^(β―βπ))) |
68 | 65, 67 | ffvelcdmd 7085 |
. . . . . . . . . . . 12
β’ (π β (πβπΌ) β π) |
69 | 4, 42 | unitgrpbas 20189 |
. . . . . . . . . . . . 13
β’ π = (Baseβπ») |
70 | 69, 46 | odcl2 19428 |
. . . . . . . . . . . 12
β’ ((π» β Grp β§ π β Fin β§ (πβπΌ) β π) β (πβ(πβπΌ)) β β) |
71 | 58, 63, 68, 70 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (πβ(πβπΌ)) β β) |
72 | | nndivre 12250 |
. . . . . . . . . . 11
β’ ((2
β β β§ (πβ(πβπΌ)) β β) β (2 / (πβ(πβπΌ))) β β) |
73 | 52, 71, 72 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (2 / (πβ(πβπΌ))) β β) |
74 | 73 | recnd 11239 |
. . . . . . . . 9
β’ (π β (2 / (πβ(πβπΌ))) β β) |
75 | | cxpcl 26174 |
. . . . . . . . 9
β’ ((-1
β β β§ (2 / (πβ(πβπΌ))) β β) β
(-1βπ(2 / (πβ(πβπΌ)))) β β) |
76 | 51, 74, 75 | sylancr 588 |
. . . . . . . 8
β’ (π β
(-1βπ(2 / (πβ(πβπΌ)))) β β) |
77 | 47, 76 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π β β) |
78 | 77 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β π β β) |
79 | 51 | a1i 11 |
. . . . . . . . 9
β’ (π β -1 β
β) |
80 | | neg1ne0 12325 |
. . . . . . . . . 10
β’ -1 β
0 |
81 | 80 | a1i 11 |
. . . . . . . . 9
β’ (π β -1 β
0) |
82 | 79, 81, 74 | cxpne0d 26213 |
. . . . . . . 8
β’ (π β
(-1βπ(2 / (πβ(πβπΌ)))) β 0) |
83 | 47 | neeq1i 3006 |
. . . . . . . 8
β’ (π β 0 β
(-1βπ(2 / (πβ(πβπΌ)))) β 0) |
84 | 82, 83 | sylibr 233 |
. . . . . . 7
β’ (π β π β 0) |
85 | 84 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β π β 0) |
86 | | simprl 770 |
. . . . . 6
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β π β β€) |
87 | 78, 85, 86 | expclzd 14113 |
. . . . 5
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β (πβπ) β β) |
88 | 50, 87 | eqeltrd 2834 |
. . . 4
β’ (((π β§ π£ β π) β§ (π β β€ β§ ((πβπΌ)βπ£) = (π Β· (πβπΌ)))) β (πβπ£) β β) |
89 | 39, 88 | rexlimddv 3162 |
. . 3
β’ ((π β§ π£ β π) β (πβπ£) β β) |
90 | | fveqeq2 6898 |
. . . . . 6
β’ (π£ = π₯ β (((πβπΌ)βπ£) = (π Β· (πβπΌ)) β ((πβπΌ)βπ₯) = (π Β· (πβπΌ)))) |
91 | 90 | rexbidv 3179 |
. . . . 5
β’ (π£ = π₯ β (βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ)) β βπ β β€ ((πβπΌ)βπ₯) = (π Β· (πβπΌ)))) |
92 | 39 | ralrimiva 3147 |
. . . . . 6
β’ (π β βπ£ β π βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ))) |
93 | 92 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β βπ£ β π βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ))) |
94 | | simprl 770 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π₯ β π) |
95 | 91, 93, 94 | rspcdva 3614 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β βπ β β€ ((πβπΌ)βπ₯) = (π Β· (πβπΌ))) |
96 | | fveqeq2 6898 |
. . . . . . 7
β’ (π£ = π¦ β (((πβπΌ)βπ£) = (π Β· (πβπΌ)) β ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) |
97 | 96 | rexbidv 3179 |
. . . . . 6
β’ (π£ = π¦ β (βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ)) β βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) |
98 | | oveq1 7413 |
. . . . . . . 8
β’ (π = π β (π Β· (πβπΌ)) = (π Β· (πβπΌ))) |
99 | 98 | eqeq2d 2744 |
. . . . . . 7
β’ (π = π β (((πβπΌ)βπ¦) = (π Β· (πβπΌ)) β ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) |
100 | 99 | cbvrexvw 3236 |
. . . . . 6
β’
(βπ β
β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ)) β βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) |
101 | 97, 100 | bitrdi 287 |
. . . . 5
β’ (π£ = π¦ β (βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ)) β βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) |
102 | | simprr 772 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β π¦ β π) |
103 | 101, 93, 102 | rspcdva 3614 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) |
104 | | reeanv 3227 |
. . . . 5
β’
(βπ β
β€ βπ β
β€ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) β (βπ β β€ ((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) |
105 | 77 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π β β) |
106 | 84 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π β 0) |
107 | | simprll 778 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π β β€) |
108 | | simprlr 779 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π β β€) |
109 | | expaddz 14069 |
. . . . . . . . 9
β’ (((π β β β§ π β 0) β§ (π β β€ β§ π β β€)) β (πβ(π + π)) = ((πβπ) Β· (πβπ))) |
110 | 105, 106,
107, 108, 109 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβ(π + π)) = ((πβπ) Β· (πβπ))) |
111 | | simpll 766 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π) |
112 | 56 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π β Ring) |
113 | 94 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π₯ β π) |
114 | 102 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π¦ β π) |
115 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.rβπ) = (.rβπ) |
116 | 4, 115 | unitmulcl 20187 |
. . . . . . . . . 10
β’ ((π β Ring β§ π₯ β π β§ π¦ β π) β (π₯(.rβπ)π¦) β π) |
117 | 112, 113,
114, 116 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (π₯(.rβπ)π¦) β π) |
118 | 107, 108 | zaddcld 12667 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (π + π) β β€) |
119 | | simprrl 780 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((πβπΌ)βπ₯) = (π Β· (πβπΌ))) |
120 | | simprrr 781 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) |
121 | 119, 120 | oveq12d 7424 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (((πβπΌ)βπ₯)(.rβπ)((πβπΌ)βπ¦)) = ((π Β· (πβπΌ))(.rβπ)(π Β· (πβπΌ)))) |
122 | 11, 17, 18, 19 | dpjghm 19928 |
. . . . . . . . . . . . 13
β’ (π β (πβπΌ) β ((π» βΎs (π» DProd π)) GrpHom π»)) |
123 | 21 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
β’ (π β (π» βΎs (π» DProd π)) = (π» βΎs π)) |
124 | 42 | ovexi 7440 |
. . . . . . . . . . . . . . . 16
β’ π» β V |
125 | 69 | ressid 17186 |
. . . . . . . . . . . . . . . 16
β’ (π» β V β (π» βΎs π) = π») |
126 | 124, 125 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (π» βΎs π) = π» |
127 | 123, 126 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (π β (π» βΎs (π» DProd π)) = π») |
128 | 127 | oveq1d 7421 |
. . . . . . . . . . . . 13
β’ (π β ((π» βΎs (π» DProd π)) GrpHom π») = (π» GrpHom π»)) |
129 | 122, 128 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ (π β (πβπΌ) β (π» GrpHom π»)) |
130 | 129 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβπΌ) β (π» GrpHom π»)) |
131 | 4 | fvexi 6903 |
. . . . . . . . . . . . 13
β’ π β V |
132 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(mulGrpβπ) =
(mulGrpβπ) |
133 | 132, 115 | mgpplusg 19986 |
. . . . . . . . . . . . . 14
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
134 | 42, 133 | ressplusg 17232 |
. . . . . . . . . . . . 13
β’ (π β V β
(.rβπ) =
(+gβπ»)) |
135 | 131, 134 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(.rβπ) = (+gβπ») |
136 | 69, 135, 135 | ghmlin 19092 |
. . . . . . . . . . 11
β’ (((πβπΌ) β (π» GrpHom π») β§ π₯ β π β§ π¦ β π) β ((πβπΌ)β(π₯(.rβπ)π¦)) = (((πβπΌ)βπ₯)(.rβπ)((πβπΌ)βπ¦))) |
137 | 130, 113,
114, 136 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((πβπΌ)β(π₯(.rβπ)π¦)) = (((πβπΌ)βπ₯)(.rβπ)((πβπΌ)βπ¦))) |
138 | 58 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β π» β Grp) |
139 | 68 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβπΌ) β π) |
140 | 69, 43, 135 | mulgdir 18981 |
. . . . . . . . . . 11
β’ ((π» β Grp β§ (π β β€ β§ π β β€ β§ (πβπΌ) β π)) β ((π + π) Β· (πβπΌ)) = ((π Β· (πβπΌ))(.rβπ)(π Β· (πβπΌ)))) |
141 | 138, 107,
108, 139, 140 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((π + π) Β· (πβπΌ)) = ((π Β· (πβπΌ))(.rβπ)(π Β· (πβπΌ)))) |
142 | 121, 137,
141 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((πβπΌ)β(π₯(.rβπ)π¦)) = ((π + π) Β· (πβπΌ))) |
143 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . . . . . 9
β’ (((π β§ (π₯(.rβπ)π¦) β π) β§ ((π + π) β β€ β§ ((πβπΌ)β(π₯(.rβπ)π¦)) = ((π + π) Β· (πβπΌ)))) β (πβ(π₯(.rβπ)π¦)) = (πβ(π + π))) |
144 | 111, 117,
118, 142, 143 | syl22anc 838 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβ(π₯(.rβπ)π¦)) = (πβ(π + π))) |
145 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ (π β β€ β§ ((πβπΌ)βπ₯) = (π Β· (πβπΌ)))) β (πβπ₯) = (πβπ)) |
146 | 111, 113,
107, 119, 145 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβπ₯) = (πβπ)) |
147 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β β€ β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ)))) β (πβπ¦) = (πβπ)) |
148 | 111, 114,
108, 120, 147 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβπ¦) = (πβπ)) |
149 | 146, 148 | oveq12d 7424 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β ((πβπ₯) Β· (πβπ¦)) = ((πβπ) Β· (πβπ))) |
150 | 110, 144,
149 | 3eqtr4d 2783 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ ((π β β€ β§ π β β€) β§ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
151 | 150 | expr 458 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β π)) β§ (π β β€ β§ π β β€)) β ((((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
152 | 151 | rexlimdvva 3212 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (βπ β β€ βπ β β€ (((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
153 | 104, 152 | biimtrrid 242 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((βπ β β€ ((πβπΌ)βπ₯) = (π Β· (πβπΌ)) β§ βπ β β€ ((πβπΌ)βπ¦) = (π Β· (πβπΌ))) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦)))) |
154 | 95, 103, 153 | mp2and 698 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πβ(π₯(.rβπ)π¦)) = ((πβπ₯) Β· (πβπ¦))) |
155 | | id 22 |
. . . . 5
β’ (π β π) |
156 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
157 | 4, 156 | 1unit 20181 |
. . . . . 6
β’ (π β Ring β
(1rβπ)
β π) |
158 | 56, 157 | syl 17 |
. . . . 5
β’ (π β (1rβπ) β π) |
159 | | 0zd 12567 |
. . . . 5
β’ (π β 0 β
β€) |
160 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ») = (0gβπ») |
161 | 160, 160 | ghmid 19093 |
. . . . . . 7
β’ ((πβπΌ) β (π» GrpHom π») β ((πβπΌ)β(0gβπ»)) = (0gβπ»)) |
162 | 129, 161 | syl 17 |
. . . . . 6
β’ (π β ((πβπΌ)β(0gβπ»)) = (0gβπ»)) |
163 | 4, 42, 156 | unitgrpid 20192 |
. . . . . . . 8
β’ (π β Ring β
(1rβπ) =
(0gβπ»)) |
164 | 56, 163 | syl 17 |
. . . . . . 7
β’ (π β (1rβπ) = (0gβπ»)) |
165 | 164 | fveq2d 6893 |
. . . . . 6
β’ (π β ((πβπΌ)β(1rβπ)) = ((πβπΌ)β(0gβπ»))) |
166 | 69, 160, 43 | mulg0 18952 |
. . . . . . 7
β’ ((πβπΌ) β π β (0 Β· (πβπΌ)) = (0gβπ»)) |
167 | 68, 166 | syl 17 |
. . . . . 6
β’ (π β (0 Β· (πβπΌ)) = (0gβπ»)) |
168 | 162, 165,
167 | 3eqtr4d 2783 |
. . . . 5
β’ (π β ((πβπΌ)β(1rβπ)) = (0 Β· (πβπΌ))) |
169 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . 5
β’ (((π β§ (1rβπ) β π) β§ (0 β β€ β§ ((πβπΌ)β(1rβπ)) = (0 Β· (πβπΌ)))) β (πβ(1rβπ)) = (πβ0)) |
170 | 155, 158,
159, 168, 169 | syl22anc 838 |
. . . 4
β’ (π β (πβ(1rβπ)) = (πβ0)) |
171 | 77 | exp0d 14102 |
. . . 4
β’ (π β (πβ0) = 1) |
172 | 170, 171 | eqtrd 2773 |
. . 3
β’ (π β (πβ(1rβπ)) = 1) |
173 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
89, 154, 172 | dchrelbasd 26732 |
. 2
β’ (π β (π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) β π·) |
174 | 61, 44 | sselid 3980 |
. . . . 5
β’ (π β π΄ β π΅) |
175 | | eleq1 2822 |
. . . . . . 7
β’ (π£ = π΄ β (π£ β π β π΄ β π)) |
176 | | fveq2 6889 |
. . . . . . 7
β’ (π£ = π΄ β (πβπ£) = (πβπ΄)) |
177 | 175, 176 | ifbieq1d 4552 |
. . . . . 6
β’ (π£ = π΄ β if(π£ β π, (πβπ£), 0) = if(π΄ β π, (πβπ΄), 0)) |
178 | | eqid 2733 |
. . . . . 6
β’ (π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) = (π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) |
179 | | fvex 6902 |
. . . . . . 7
β’ (πβπ£) β V |
180 | | c0ex 11205 |
. . . . . . 7
β’ 0 β
V |
181 | 179, 180 | ifex 4578 |
. . . . . 6
β’ if(π£ β π, (πβπ£), 0) β V |
182 | 177, 178,
181 | fvmpt3i 7001 |
. . . . 5
β’ (π΄ β π΅ β ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) = if(π΄ β π, (πβπ΄), 0)) |
183 | 174, 182 | syl 17 |
. . . 4
β’ (π β ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) = if(π΄ β π, (πβπ΄), 0)) |
184 | 44 | iftrued 4536 |
. . . 4
β’ (π β if(π΄ β π, (πβπ΄), 0) = (πβπ΄)) |
185 | 183, 184 | eqtrd 2773 |
. . 3
β’ (π β ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) = (πβπ΄)) |
186 | | fveqeq2 6898 |
. . . . . 6
β’ (π£ = π΄ β (((πβπΌ)βπ£) = (π Β· (πβπΌ)) β ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) |
187 | 186 | rexbidv 3179 |
. . . . 5
β’ (π£ = π΄ β (βπ β β€ ((πβπΌ)βπ£) = (π Β· (πβπΌ)) β βπ β β€ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) |
188 | 187, 92, 44 | rspcdva 3614 |
. . . 4
β’ (π β βπ β β€ ((πβπΌ)βπ΄) = (π Β· (πβπΌ))) |
189 | 1, 2, 6, 3, 40, 5,
41, 4, 42, 43, 15, 44, 45, 11, 21, 18, 46, 47, 19, 48, 49 | dchrptlem1 26757 |
. . . . . . . 8
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (πβπ΄) = (πβπ)) |
190 | 47 | oveq1i 7416 |
. . . . . . . 8
β’ (πβπ) = ((-1βπ(2 / (πβ(πβπΌ))))βπ) |
191 | 189, 190 | eqtrdi 2789 |
. . . . . . 7
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (πβπ΄) = ((-1βπ(2 /
(πβ(πβπΌ))))βπ)) |
192 | 48 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β ((πβπΌ)βπ΄) β 1 ) |
193 | 58 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β π» β Grp) |
194 | 68 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (πβπΌ) β π) |
195 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β π β β€) |
196 | 69, 46, 43, 160 | oddvds 19410 |
. . . . . . . . . . 11
β’ ((π» β Grp β§ (πβπΌ) β π β§ π β β€) β ((πβ(πβπΌ)) β₯ π β (π Β· (πβπΌ)) = (0gβπ»))) |
197 | 193, 194,
195, 196 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β ((πβ(πβπΌ)) β₯ π β (π Β· (πβπΌ)) = (0gβπ»))) |
198 | 71 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (πβ(πβπΌ)) β β) |
199 | | root1eq1 26253 |
. . . . . . . . . . 11
β’ (((πβ(πβπΌ)) β β β§ π β β€) β
(((-1βπ(2 / (πβ(πβπΌ))))βπ) = 1 β (πβ(πβπΌ)) β₯ π)) |
200 | 198, 195,
199 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β
(((-1βπ(2 / (πβ(πβπΌ))))βπ) = 1 β (πβ(πβπΌ)) β₯ π)) |
201 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β ((πβπΌ)βπ΄) = (π Β· (πβπΌ))) |
202 | 40, 164 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π β 1 =
(0gβπ»)) |
203 | 202 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β 1 =
(0gβπ»)) |
204 | 201, 203 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (((πβπΌ)βπ΄) = 1 β (π Β· (πβπΌ)) = (0gβπ»))) |
205 | 197, 200,
204 | 3bitr4d 311 |
. . . . . . . . 9
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β
(((-1βπ(2 / (πβ(πβπΌ))))βπ) = 1 β ((πβπΌ)βπ΄) = 1 )) |
206 | 205 | necon3bid 2986 |
. . . . . . . 8
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β
(((-1βπ(2 / (πβ(πβπΌ))))βπ) β 1 β ((πβπΌ)βπ΄) β 1 )) |
207 | 192, 206 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β ((-1βπ(2
/ (πβ(πβπΌ))))βπ) β 1) |
208 | 191, 207 | eqnetrd 3009 |
. . . . . 6
β’ (((π β§ π΄ β π) β§ (π β β€ β§ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)))) β (πβπ΄) β 1) |
209 | 208 | rexlimdvaa 3157 |
. . . . 5
β’ ((π β§ π΄ β π) β (βπ β β€ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)) β (πβπ΄) β 1)) |
210 | 44, 209 | mpdan 686 |
. . . 4
β’ (π β (βπ β β€ ((πβπΌ)βπ΄) = (π Β· (πβπΌ)) β (πβπ΄) β 1)) |
211 | 188, 210 | mpd 15 |
. . 3
β’ (π β (πβπ΄) β 1) |
212 | 185, 211 | eqnetrd 3009 |
. 2
β’ (π β ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) β 1) |
213 | | fveq1 6888 |
. . . 4
β’ (π₯ = (π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) β (π₯βπ΄) = ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄)) |
214 | 213 | neeq1d 3001 |
. . 3
β’ (π₯ = (π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) β ((π₯βπ΄) β 1 β ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) β 1)) |
215 | 214 | rspcev 3613 |
. 2
β’ (((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0)) β π· β§ ((π£ β π΅ β¦ if(π£ β π, (πβπ£), 0))βπ΄) β 1) β βπ₯ β π· (π₯βπ΄) β 1) |
216 | 173, 212,
215 | syl2anc 585 |
1
β’ (π β βπ₯ β π· (π₯βπ΄) β 1) |