Step |
Hyp |
Ref |
Expression |
1 |
|
dchrabs.g |
|- G = ( DChr ` N ) |
2 |
|
dchrabs.d |
|- D = ( Base ` G ) |
3 |
|
dchrabs.x |
|- ( ph -> X e. D ) |
4 |
|
dchrabs.z |
|- Z = ( Z/nZ ` N ) |
5 |
|
dchrabs.u |
|- U = ( Unit ` Z ) |
6 |
|
dchrabs.a |
|- ( ph -> A e. U ) |
7 |
|
eqid |
|- ( Base ` Z ) = ( Base ` Z ) |
8 |
1 4 2 7 3
|
dchrf |
|- ( ph -> X : ( Base ` Z ) --> CC ) |
9 |
7 5
|
unitss |
|- U C_ ( Base ` Z ) |
10 |
9 6
|
sselid |
|- ( ph -> A e. ( Base ` Z ) ) |
11 |
8 10
|
ffvelrnd |
|- ( ph -> ( X ` A ) e. CC ) |
12 |
1 4 2 7 5 3 10
|
dchrn0 |
|- ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) ) |
13 |
6 12
|
mpbird |
|- ( ph -> ( X ` A ) =/= 0 ) |
14 |
11 13
|
absrpcld |
|- ( ph -> ( abs ` ( X ` A ) ) e. RR+ ) |
15 |
1 2
|
dchrrcl |
|- ( X e. D -> N e. NN ) |
16 |
4 7
|
znfi |
|- ( N e. NN -> ( Base ` Z ) e. Fin ) |
17 |
3 15 16
|
3syl |
|- ( ph -> ( Base ` Z ) e. Fin ) |
18 |
|
ssfi |
|- ( ( ( Base ` Z ) e. Fin /\ U C_ ( Base ` Z ) ) -> U e. Fin ) |
19 |
17 9 18
|
sylancl |
|- ( ph -> U e. Fin ) |
20 |
|
hashcl |
|- ( U e. Fin -> ( # ` U ) e. NN0 ) |
21 |
19 20
|
syl |
|- ( ph -> ( # ` U ) e. NN0 ) |
22 |
21
|
nn0red |
|- ( ph -> ( # ` U ) e. RR ) |
23 |
22
|
recnd |
|- ( ph -> ( # ` U ) e. CC ) |
24 |
6
|
ne0d |
|- ( ph -> U =/= (/) ) |
25 |
|
hashnncl |
|- ( U e. Fin -> ( ( # ` U ) e. NN <-> U =/= (/) ) ) |
26 |
19 25
|
syl |
|- ( ph -> ( ( # ` U ) e. NN <-> U =/= (/) ) ) |
27 |
24 26
|
mpbird |
|- ( ph -> ( # ` U ) e. NN ) |
28 |
27
|
nnne0d |
|- ( ph -> ( # ` U ) =/= 0 ) |
29 |
23 28
|
reccld |
|- ( ph -> ( 1 / ( # ` U ) ) e. CC ) |
30 |
14 22 29
|
cxpmuld |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) ) = ( ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) ^c ( 1 / ( # ` U ) ) ) ) |
31 |
23 28
|
recidd |
|- ( ph -> ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) = 1 ) |
32 |
31
|
oveq2d |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c ( ( # ` U ) x. ( 1 / ( # ` U ) ) ) ) = ( ( abs ` ( X ` A ) ) ^c 1 ) ) |
33 |
11
|
abscld |
|- ( ph -> ( abs ` ( X ` A ) ) e. RR ) |
34 |
33
|
recnd |
|- ( ph -> ( abs ` ( X ` A ) ) e. CC ) |
35 |
|
cxpexp |
|- ( ( ( abs ` ( X ` A ) ) e. CC /\ ( # ` U ) e. NN0 ) -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) ) |
36 |
34 21 35
|
syl2anc |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) ) |
37 |
11 21
|
absexpd |
|- ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = ( ( abs ` ( X ` A ) ) ^ ( # ` U ) ) ) |
38 |
|
cnring |
|- CCfld e. Ring |
39 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
40 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
41 |
|
cndrng |
|- CCfld e. DivRing |
42 |
39 40 41
|
drngui |
|- ( CC \ { 0 } ) = ( Unit ` CCfld ) |
43 |
|
eqid |
|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld ) |
44 |
42 43
|
unitsubm |
|- ( CCfld e. Ring -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
45 |
38 44
|
mp1i |
|- ( ph -> ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) ) |
46 |
|
eldifsn |
|- ( ( X ` A ) e. ( CC \ { 0 } ) <-> ( ( X ` A ) e. CC /\ ( X ` A ) =/= 0 ) ) |
47 |
11 13 46
|
sylanbrc |
|- ( ph -> ( X ` A ) e. ( CC \ { 0 } ) ) |
48 |
|
eqid |
|- ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) ) |
49 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
50 |
|
eqid |
|- ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) = ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) |
51 |
48 49 50
|
submmulg |
|- ( ( ( CC \ { 0 } ) e. ( SubMnd ` ( mulGrp ` CCfld ) ) /\ ( # ` U ) e. NN0 /\ ( X ` A ) e. ( CC \ { 0 } ) ) -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) ) |
52 |
45 21 47 51
|
syl3anc |
|- ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) ) |
53 |
|
eqid |
|- ( ( mulGrp ` Z ) |`s U ) = ( ( mulGrp ` Z ) |`s U ) |
54 |
1 4 2 5 53 49 3
|
dchrghm |
|- ( ph -> ( X |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ) |
55 |
21
|
nn0zd |
|- ( ph -> ( # ` U ) e. ZZ ) |
56 |
5 53
|
unitgrpbas |
|- U = ( Base ` ( ( mulGrp ` Z ) |`s U ) ) |
57 |
|
eqid |
|- ( .g ` ( ( mulGrp ` Z ) |`s U ) ) = ( .g ` ( ( mulGrp ` Z ) |`s U ) ) |
58 |
56 57 50
|
ghmmulg |
|- ( ( ( X |` U ) e. ( ( ( mulGrp ` Z ) |`s U ) GrpHom ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) /\ ( # ` U ) e. ZZ /\ A e. U ) -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) ) |
59 |
54 55 6 58
|
syl3anc |
|- ( ph -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) ) |
60 |
3 15
|
syl |
|- ( ph -> N e. NN ) |
61 |
60
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
62 |
4
|
zncrng |
|- ( N e. NN0 -> Z e. CRing ) |
63 |
|
crngring |
|- ( Z e. CRing -> Z e. Ring ) |
64 |
61 62 63
|
3syl |
|- ( ph -> Z e. Ring ) |
65 |
5 53
|
unitgrp |
|- ( Z e. Ring -> ( ( mulGrp ` Z ) |`s U ) e. Grp ) |
66 |
64 65
|
syl |
|- ( ph -> ( ( mulGrp ` Z ) |`s U ) e. Grp ) |
67 |
|
eqid |
|- ( od ` ( ( mulGrp ` Z ) |`s U ) ) = ( od ` ( ( mulGrp ` Z ) |`s U ) ) |
68 |
56 67
|
oddvds2 |
|- ( ( ( ( mulGrp ` Z ) |`s U ) e. Grp /\ U e. Fin /\ A e. U ) -> ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) ) |
69 |
66 19 6 68
|
syl3anc |
|- ( ph -> ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) ) |
70 |
|
eqid |
|- ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) |
71 |
56 67 57 70
|
oddvds |
|- ( ( ( ( mulGrp ` Z ) |`s U ) e. Grp /\ A e. U /\ ( # ` U ) e. ZZ ) -> ( ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) <-> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) ) |
72 |
66 6 55 71
|
syl3anc |
|- ( ph -> ( ( ( od ` ( ( mulGrp ` Z ) |`s U ) ) ` A ) || ( # ` U ) <-> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) ) |
73 |
69 72
|
mpbid |
|- ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) |
74 |
|
eqid |
|- ( 1r ` Z ) = ( 1r ` Z ) |
75 |
5 53 74
|
unitgrpid |
|- ( Z e. Ring -> ( 1r ` Z ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) |
76 |
64 75
|
syl |
|- ( ph -> ( 1r ` Z ) = ( 0g ` ( ( mulGrp ` Z ) |`s U ) ) ) |
77 |
73 76
|
eqtr4d |
|- ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) = ( 1r ` Z ) ) |
78 |
77
|
fveq2d |
|- ( ph -> ( ( X |` U ) ` ( ( # ` U ) ( .g ` ( ( mulGrp ` Z ) |`s U ) ) A ) ) = ( ( X |` U ) ` ( 1r ` Z ) ) ) |
79 |
6
|
fvresd |
|- ( ph -> ( ( X |` U ) ` A ) = ( X ` A ) ) |
80 |
79
|
oveq2d |
|- ( ph -> ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( ( X |` U ) ` A ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) ) |
81 |
59 78 80
|
3eqtr3d |
|- ( ph -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( ( # ` U ) ( .g ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) ( X ` A ) ) ) |
82 |
5 74
|
1unit |
|- ( Z e. Ring -> ( 1r ` Z ) e. U ) |
83 |
|
fvres |
|- ( ( 1r ` Z ) e. U -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( X ` ( 1r ` Z ) ) ) |
84 |
64 82 83
|
3syl |
|- ( ph -> ( ( X |` U ) ` ( 1r ` Z ) ) = ( X ` ( 1r ` Z ) ) ) |
85 |
52 81 84
|
3eqtr2d |
|- ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( X ` ( 1r ` Z ) ) ) |
86 |
|
cnfldexp |
|- ( ( ( X ` A ) e. CC /\ ( # ` U ) e. NN0 ) -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( X ` A ) ^ ( # ` U ) ) ) |
87 |
11 21 86
|
syl2anc |
|- ( ph -> ( ( # ` U ) ( .g ` ( mulGrp ` CCfld ) ) ( X ` A ) ) = ( ( X ` A ) ^ ( # ` U ) ) ) |
88 |
1 4 2
|
dchrmhm |
|- D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) |
89 |
88 3
|
sselid |
|- ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) |
90 |
|
eqid |
|- ( mulGrp ` Z ) = ( mulGrp ` Z ) |
91 |
90 74
|
ringidval |
|- ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) ) |
92 |
|
cnfld1 |
|- 1 = ( 1r ` CCfld ) |
93 |
43 92
|
ringidval |
|- 1 = ( 0g ` ( mulGrp ` CCfld ) ) |
94 |
91 93
|
mhm0 |
|- ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 ) |
95 |
89 94
|
syl |
|- ( ph -> ( X ` ( 1r ` Z ) ) = 1 ) |
96 |
85 87 95
|
3eqtr3d |
|- ( ph -> ( ( X ` A ) ^ ( # ` U ) ) = 1 ) |
97 |
96
|
fveq2d |
|- ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = ( abs ` 1 ) ) |
98 |
|
abs1 |
|- ( abs ` 1 ) = 1 |
99 |
97 98
|
eqtrdi |
|- ( ph -> ( abs ` ( ( X ` A ) ^ ( # ` U ) ) ) = 1 ) |
100 |
36 37 99
|
3eqtr2d |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) = 1 ) |
101 |
100
|
oveq1d |
|- ( ph -> ( ( ( abs ` ( X ` A ) ) ^c ( # ` U ) ) ^c ( 1 / ( # ` U ) ) ) = ( 1 ^c ( 1 / ( # ` U ) ) ) ) |
102 |
30 32 101
|
3eqtr3d |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c 1 ) = ( 1 ^c ( 1 / ( # ` U ) ) ) ) |
103 |
34
|
cxp1d |
|- ( ph -> ( ( abs ` ( X ` A ) ) ^c 1 ) = ( abs ` ( X ` A ) ) ) |
104 |
29
|
1cxpd |
|- ( ph -> ( 1 ^c ( 1 / ( # ` U ) ) ) = 1 ) |
105 |
102 103 104
|
3eqtr3d |
|- ( ph -> ( abs ` ( X ` A ) ) = 1 ) |