Step | Hyp | Ref
| Expression |
1 | | dchrabs.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
2 | | dchrabs.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
3 | | dchrabs.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
4 | | eqid 2737 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
5 | | dchrabs.x |
. . . . . . 7
β’ (π β π β π·) |
6 | 1, 2, 3, 4, 5 | dchrf 26606 |
. . . . . 6
β’ (π β π:(Baseβπ)βΆβ) |
7 | | dchrabs.u |
. . . . . . . 8
β’ π = (Unitβπ) |
8 | 4, 7 | unitss 20096 |
. . . . . . 7
β’ π β (Baseβπ) |
9 | | dchrabs.a |
. . . . . . 7
β’ (π β π΄ β π) |
10 | 8, 9 | sselid 3947 |
. . . . . 6
β’ (π β π΄ β (Baseβπ)) |
11 | 6, 10 | ffvelcdmd 7041 |
. . . . 5
β’ (π β (πβπ΄) β β) |
12 | 1, 2, 3, 4, 7, 5, 10 | dchrn0 26614 |
. . . . . 6
β’ (π β ((πβπ΄) β 0 β π΄ β π)) |
13 | 9, 12 | mpbird 257 |
. . . . 5
β’ (π β (πβπ΄) β 0) |
14 | 11, 13 | absrpcld 15340 |
. . . 4
β’ (π β (absβ(πβπ΄)) β
β+) |
15 | 1, 3 | dchrrcl 26604 |
. . . . . . . 8
β’ (π β π· β π β β) |
16 | 2, 4 | znfi 20982 |
. . . . . . . 8
β’ (π β β β
(Baseβπ) β
Fin) |
17 | 5, 15, 16 | 3syl 18 |
. . . . . . 7
β’ (π β (Baseβπ) β Fin) |
18 | | ssfi 9124 |
. . . . . . 7
β’
(((Baseβπ)
β Fin β§ π β
(Baseβπ)) β
π β
Fin) |
19 | 17, 8, 18 | sylancl 587 |
. . . . . 6
β’ (π β π β Fin) |
20 | | hashcl 14263 |
. . . . . 6
β’ (π β Fin β
(β―βπ) β
β0) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ (π β (β―βπ) β
β0) |
22 | 21 | nn0red 12481 |
. . . 4
β’ (π β (β―βπ) β
β) |
23 | 22 | recnd 11190 |
. . . . 5
β’ (π β (β―βπ) β
β) |
24 | 9 | ne0d 4300 |
. . . . . . 7
β’ (π β π β β
) |
25 | | hashnncl 14273 |
. . . . . . . 8
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
26 | 19, 25 | syl 17 |
. . . . . . 7
β’ (π β ((β―βπ) β β β π β β
)) |
27 | 24, 26 | mpbird 257 |
. . . . . 6
β’ (π β (β―βπ) β
β) |
28 | 27 | nnne0d 12210 |
. . . . 5
β’ (π β (β―βπ) β 0) |
29 | 23, 28 | reccld 11931 |
. . . 4
β’ (π β (1 / (β―βπ)) β
β) |
30 | 14, 22, 29 | cxpmuld 26107 |
. . 3
β’ (π β ((absβ(πβπ΄))βπ((β―βπ) Β· (1 / (β―βπ)))) = (((absβ(πβπ΄))βπ(β―βπ))βπ(1 /
(β―βπ)))) |
31 | 23, 28 | recidd 11933 |
. . . 4
β’ (π β ((β―βπ) Β· (1 /
(β―βπ))) =
1) |
32 | 31 | oveq2d 7378 |
. . 3
β’ (π β ((absβ(πβπ΄))βπ((β―βπ) Β· (1 / (β―βπ)))) = ((absβ(πβπ΄))βπ1)) |
33 | 11 | abscld 15328 |
. . . . . . 7
β’ (π β (absβ(πβπ΄)) β β) |
34 | 33 | recnd 11190 |
. . . . . 6
β’ (π β (absβ(πβπ΄)) β β) |
35 | | cxpexp 26039 |
. . . . . 6
β’
(((absβ(πβπ΄)) β β β§ (β―βπ) β β0)
β ((absβ(πβπ΄))βπ(β―βπ)) = ((absβ(πβπ΄))β(β―βπ))) |
36 | 34, 21, 35 | syl2anc 585 |
. . . . 5
β’ (π β ((absβ(πβπ΄))βπ(β―βπ)) = ((absβ(πβπ΄))β(β―βπ))) |
37 | 11, 21 | absexpd 15344 |
. . . . 5
β’ (π β (absβ((πβπ΄)β(β―βπ))) = ((absβ(πβπ΄))β(β―βπ))) |
38 | | cnring 20835 |
. . . . . . . . . . 11
β’
βfld β Ring |
39 | | cnfldbas 20816 |
. . . . . . . . . . . . 13
β’ β =
(Baseββfld) |
40 | | cnfld0 20837 |
. . . . . . . . . . . . 13
β’ 0 =
(0gββfld) |
41 | | cndrng 20842 |
. . . . . . . . . . . . 13
β’
βfld β DivRing |
42 | 39, 40, 41 | drngui 20205 |
. . . . . . . . . . . 12
β’ (β
β {0}) = (Unitββfld) |
43 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(mulGrpββfld) =
(mulGrpββfld) |
44 | 42, 43 | unitsubm 20106 |
. . . . . . . . . . 11
β’
(βfld β Ring β (β β {0}) β
(SubMndβ(mulGrpββfld))) |
45 | 38, 44 | mp1i 13 |
. . . . . . . . . 10
β’ (π β (β β {0})
β (SubMndβ(mulGrpββfld))) |
46 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ ((πβπ΄) β (β β {0}) β
((πβπ΄) β β β§ (πβπ΄) β 0)) |
47 | 11, 13, 46 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β (πβπ΄) β (β β
{0})) |
48 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
49 | | eqid 2737 |
. . . . . . . . . . 11
β’
((mulGrpββfld) βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
50 | | eqid 2737 |
. . . . . . . . . . 11
β’
(.gβ((mulGrpββfld)
βΎs (β β {0}))) =
(.gβ((mulGrpββfld) βΎs
(β β {0}))) |
51 | 48, 49, 50 | submmulg 18927 |
. . . . . . . . . 10
β’
(((β β {0}) β
(SubMndβ(mulGrpββfld)) β§ (β―βπ) β β0
β§ (πβπ΄) β (β β {0}))
β ((β―βπ)(.gβ(mulGrpββfld))(πβπ΄)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))(πβπ΄))) |
52 | 45, 21, 47, 51 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((β―βπ)(.gβ(mulGrpββfld))(πβπ΄)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))(πβπ΄))) |
53 | | eqid 2737 |
. . . . . . . . . . . 12
β’
((mulGrpβπ)
βΎs π) =
((mulGrpβπ)
βΎs π) |
54 | 1, 2, 3, 7, 53, 49, 5 | dchrghm 26620 |
. . . . . . . . . . 11
β’ (π β (π βΎ π) β (((mulGrpβπ) βΎs π) GrpHom
((mulGrpββfld) βΎs (β β
{0})))) |
55 | 21 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (π β (β―βπ) β
β€) |
56 | 7, 53 | unitgrpbas 20102 |
. . . . . . . . . . . 12
β’ π =
(Baseβ((mulGrpβπ) βΎs π)) |
57 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(.gβ((mulGrpβπ) βΎs π)) =
(.gβ((mulGrpβπ) βΎs π)) |
58 | 56, 57, 50 | ghmmulg 19027 |
. . . . . . . . . . 11
β’ (((π βΎ π) β (((mulGrpβπ) βΎs π) GrpHom
((mulGrpββfld) βΎs (β β
{0}))) β§ (β―βπ) β β€ β§ π΄ β π) β ((π βΎ π)β((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))((π βΎ π)βπ΄))) |
59 | 54, 55, 9, 58 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β ((π βΎ π)β((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))((π βΎ π)βπ΄))) |
60 | 5, 15 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
61 | 60 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
62 | 2 | zncrng 20967 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β π β
CRing) |
63 | | crngring 19983 |
. . . . . . . . . . . . . . . 16
β’ (π β CRing β π β Ring) |
64 | 61, 62, 63 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β π β Ring) |
65 | 7, 53 | unitgrp 20103 |
. . . . . . . . . . . . . . 15
β’ (π β Ring β
((mulGrpβπ)
βΎs π)
β Grp) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((mulGrpβπ) βΎs π) β Grp) |
67 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(odβ((mulGrpβπ) βΎs π)) = (odβ((mulGrpβπ) βΎs π)) |
68 | 56, 67 | oddvds2 19355 |
. . . . . . . . . . . . . 14
β’
((((mulGrpβπ)
βΎs π)
β Grp β§ π β
Fin β§ π΄ β π) β
((odβ((mulGrpβπ) βΎs π))βπ΄) β₯ (β―βπ)) |
69 | 66, 19, 9, 68 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β
((odβ((mulGrpβπ) βΎs π))βπ΄) β₯ (β―βπ)) |
70 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(0gβ((mulGrpβπ) βΎs π)) =
(0gβ((mulGrpβπ) βΎs π)) |
71 | 56, 67, 57, 70 | oddvds 19336 |
. . . . . . . . . . . . . 14
β’
((((mulGrpβπ)
βΎs π)
β Grp β§ π΄ β
π β§
(β―βπ) β
β€) β (((odβ((mulGrpβπ) βΎs π))βπ΄) β₯ (β―βπ) β ((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄) =
(0gβ((mulGrpβπ) βΎs π)))) |
72 | 66, 9, 55, 71 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β
(((odβ((mulGrpβπ) βΎs π))βπ΄) β₯ (β―βπ) β ((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄) =
(0gβ((mulGrpβπ) βΎs π)))) |
73 | 69, 72 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄) =
(0gβ((mulGrpβπ) βΎs π))) |
74 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(1rβπ) = (1rβπ) |
75 | 7, 53, 74 | unitgrpid 20105 |
. . . . . . . . . . . . 13
β’ (π β Ring β
(1rβπ) =
(0gβ((mulGrpβπ) βΎs π))) |
76 | 64, 75 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (1rβπ) =
(0gβ((mulGrpβπ) βΎs π))) |
77 | 73, 76 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (π β ((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄) = (1rβπ)) |
78 | 77 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β ((π βΎ π)β((β―βπ)(.gβ((mulGrpβπ) βΎs π))π΄)) = ((π βΎ π)β(1rβπ))) |
79 | 9 | fvresd 6867 |
. . . . . . . . . . 11
β’ (π β ((π βΎ π)βπ΄) = (πβπ΄)) |
80 | 79 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))((π βΎ π)βπ΄)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))(πβπ΄))) |
81 | 59, 78, 80 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ (π β ((π βΎ π)β(1rβπ)) = ((β―βπ)(.gβ((mulGrpββfld)
βΎs (β β {0})))(πβπ΄))) |
82 | 7, 74 | 1unit 20094 |
. . . . . . . . . 10
β’ (π β Ring β
(1rβπ)
β π) |
83 | | fvres 6866 |
. . . . . . . . . 10
β’
((1rβπ) β π β ((π βΎ π)β(1rβπ)) = (πβ(1rβπ))) |
84 | 64, 82, 83 | 3syl 18 |
. . . . . . . . 9
β’ (π β ((π βΎ π)β(1rβπ)) = (πβ(1rβπ))) |
85 | 52, 81, 84 | 3eqtr2d 2783 |
. . . . . . . 8
β’ (π β ((β―βπ)(.gβ(mulGrpββfld))(πβπ΄)) = (πβ(1rβπ))) |
86 | | cnfldexp 20846 |
. . . . . . . . 9
β’ (((πβπ΄) β β β§ (β―βπ) β β0)
β ((β―βπ)(.gβ(mulGrpββfld))(πβπ΄)) = ((πβπ΄)β(β―βπ))) |
87 | 11, 21, 86 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((β―βπ)(.gβ(mulGrpββfld))(πβπ΄)) = ((πβπ΄)β(β―βπ))) |
88 | 1, 2, 3 | dchrmhm 26605 |
. . . . . . . . . 10
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
89 | 88, 5 | sselid 3947 |
. . . . . . . . 9
β’ (π β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
90 | | eqid 2737 |
. . . . . . . . . . 11
β’
(mulGrpβπ) =
(mulGrpβπ) |
91 | 90, 74 | ringidval 19922 |
. . . . . . . . . 10
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
92 | | cnfld1 20838 |
. . . . . . . . . . 11
β’ 1 =
(1rββfld) |
93 | 43, 92 | ringidval 19922 |
. . . . . . . . . 10
β’ 1 =
(0gβ(mulGrpββfld)) |
94 | 91, 93 | mhm0 18617 |
. . . . . . . . 9
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
95 | 89, 94 | syl 17 |
. . . . . . . 8
β’ (π β (πβ(1rβπ)) = 1) |
96 | 85, 87, 95 | 3eqtr3d 2785 |
. . . . . . 7
β’ (π β ((πβπ΄)β(β―βπ)) = 1) |
97 | 96 | fveq2d 6851 |
. . . . . 6
β’ (π β (absβ((πβπ΄)β(β―βπ))) = (absβ1)) |
98 | | abs1 15189 |
. . . . . 6
β’
(absβ1) = 1 |
99 | 97, 98 | eqtrdi 2793 |
. . . . 5
β’ (π β (absβ((πβπ΄)β(β―βπ))) = 1) |
100 | 36, 37, 99 | 3eqtr2d 2783 |
. . . 4
β’ (π β ((absβ(πβπ΄))βπ(β―βπ)) = 1) |
101 | 100 | oveq1d 7377 |
. . 3
β’ (π β (((absβ(πβπ΄))βπ(β―βπ))βπ(1 /
(β―βπ))) =
(1βπ(1 / (β―βπ)))) |
102 | 30, 32, 101 | 3eqtr3d 2785 |
. 2
β’ (π β ((absβ(πβπ΄))βπ1) =
(1βπ(1 / (β―βπ)))) |
103 | 34 | cxp1d 26077 |
. 2
β’ (π β ((absβ(πβπ΄))βπ1) =
(absβ(πβπ΄))) |
104 | 29 | 1cxpd 26078 |
. 2
β’ (π β
(1βπ(1 / (β―βπ))) = 1) |
105 | 102, 103,
104 | 3eqtr3d 2785 |
1
β’ (π β (absβ(πβπ΄)) = 1) |