Metamath Proof Explorer


Theorem dchrfi

Description: The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrabl.g
|- G = ( DChr ` N )
dchrfi.b
|- D = ( Base ` G )
Assertion dchrfi
|- ( N e. NN -> D e. Fin )

Proof

Step Hyp Ref Expression
1 dchrabl.g
 |-  G = ( DChr ` N )
2 dchrfi.b
 |-  D = ( Base ` G )
3 snfi
 |-  { 0 } e. Fin
4 cnex
 |-  CC e. _V
5 4 a1i
 |-  ( N e. NN -> CC e. _V )
6 ovexd
 |-  ( ( N e. NN /\ z e. CC ) -> ( z ^ ( phi ` N ) ) e. _V )
7 1cnd
 |-  ( ( N e. NN /\ z e. CC ) -> 1 e. CC )
8 eqidd
 |-  ( N e. NN -> ( z e. CC |-> ( z ^ ( phi ` N ) ) ) = ( z e. CC |-> ( z ^ ( phi ` N ) ) ) )
9 fconstmpt
 |-  ( CC X. { 1 } ) = ( z e. CC |-> 1 )
10 9 a1i
 |-  ( N e. NN -> ( CC X. { 1 } ) = ( z e. CC |-> 1 ) )
11 5 6 7 8 10 offval2
 |-  ( N e. NN -> ( ( z e. CC |-> ( z ^ ( phi ` N ) ) ) oF - ( CC X. { 1 } ) ) = ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) )
12 ssid
 |-  CC C_ CC
13 12 a1i
 |-  ( N e. NN -> CC C_ CC )
14 1cnd
 |-  ( N e. NN -> 1 e. CC )
15 phicl
 |-  ( N e. NN -> ( phi ` N ) e. NN )
16 15 nnnn0d
 |-  ( N e. NN -> ( phi ` N ) e. NN0 )
17 plypow
 |-  ( ( CC C_ CC /\ 1 e. CC /\ ( phi ` N ) e. NN0 ) -> ( z e. CC |-> ( z ^ ( phi ` N ) ) ) e. ( Poly ` CC ) )
18 13 14 16 17 syl3anc
 |-  ( N e. NN -> ( z e. CC |-> ( z ^ ( phi ` N ) ) ) e. ( Poly ` CC ) )
19 ax-1cn
 |-  1 e. CC
20 plyconst
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> ( CC X. { 1 } ) e. ( Poly ` CC ) )
21 12 19 20 mp2an
 |-  ( CC X. { 1 } ) e. ( Poly ` CC )
22 plysubcl
 |-  ( ( ( z e. CC |-> ( z ^ ( phi ` N ) ) ) e. ( Poly ` CC ) /\ ( CC X. { 1 } ) e. ( Poly ` CC ) ) -> ( ( z e. CC |-> ( z ^ ( phi ` N ) ) ) oF - ( CC X. { 1 } ) ) e. ( Poly ` CC ) )
23 18 21 22 sylancl
 |-  ( N e. NN -> ( ( z e. CC |-> ( z ^ ( phi ` N ) ) ) oF - ( CC X. { 1 } ) ) e. ( Poly ` CC ) )
24 11 23 eqeltrrd
 |-  ( N e. NN -> ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) e. ( Poly ` CC ) )
25 0cn
 |-  0 e. CC
26 neg1ne0
 |-  -u 1 =/= 0
27 15 0expd
 |-  ( N e. NN -> ( 0 ^ ( phi ` N ) ) = 0 )
28 27 oveq1d
 |-  ( N e. NN -> ( ( 0 ^ ( phi ` N ) ) - 1 ) = ( 0 - 1 ) )
29 oveq1
 |-  ( z = 0 -> ( z ^ ( phi ` N ) ) = ( 0 ^ ( phi ` N ) ) )
30 29 oveq1d
 |-  ( z = 0 -> ( ( z ^ ( phi ` N ) ) - 1 ) = ( ( 0 ^ ( phi ` N ) ) - 1 ) )
31 eqid
 |-  ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) = ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) )
32 ovex
 |-  ( ( 0 ^ ( phi ` N ) ) - 1 ) e. _V
33 30 31 32 fvmpt
 |-  ( 0 e. CC -> ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) = ( ( 0 ^ ( phi ` N ) ) - 1 ) )
34 25 33 ax-mp
 |-  ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) = ( ( 0 ^ ( phi ` N ) ) - 1 )
35 df-neg
 |-  -u 1 = ( 0 - 1 )
36 28 34 35 3eqtr4g
 |-  ( N e. NN -> ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) = -u 1 )
37 36 neeq1d
 |-  ( N e. NN -> ( ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) =/= 0 <-> -u 1 =/= 0 ) )
38 26 37 mpbiri
 |-  ( N e. NN -> ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) =/= 0 )
39 ne0p
 |-  ( ( 0 e. CC /\ ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ` 0 ) =/= 0 ) -> ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) =/= 0p )
40 25 38 39 sylancr
 |-  ( N e. NN -> ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) =/= 0p )
41 31 mptiniseg
 |-  ( 0 e. CC -> ( `' ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) " { 0 } ) = { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } )
42 25 41 ax-mp
 |-  ( `' ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) " { 0 } ) = { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 }
43 42 eqcomi
 |-  { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } = ( `' ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) " { 0 } )
44 43 fta1
 |-  ( ( ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) e. ( Poly ` CC ) /\ ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) =/= 0p ) -> ( { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } e. Fin /\ ( # ` { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) <_ ( deg ` ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ) ) )
45 24 40 44 syl2anc
 |-  ( N e. NN -> ( { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } e. Fin /\ ( # ` { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) <_ ( deg ` ( z e. CC |-> ( ( z ^ ( phi ` N ) ) - 1 ) ) ) ) )
46 45 simpld
 |-  ( N e. NN -> { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } e. Fin )
47 unfi
 |-  ( ( { 0 } e. Fin /\ { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } e. Fin ) -> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) e. Fin )
48 3 46 47 sylancr
 |-  ( N e. NN -> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) e. Fin )
49 eqid
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
50 eqid
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
51 49 50 znfi
 |-  ( N e. NN -> ( Base ` ( Z/nZ ` N ) ) e. Fin )
52 mapfi
 |-  ( ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) e. Fin /\ ( Base ` ( Z/nZ ` N ) ) e. Fin ) -> ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ^m ( Base ` ( Z/nZ ` N ) ) ) e. Fin )
53 48 51 52 syl2anc
 |-  ( N e. NN -> ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ^m ( Base ` ( Z/nZ ` N ) ) ) e. Fin )
54 simpr
 |-  ( ( N e. NN /\ f e. D ) -> f e. D )
55 1 49 2 50 54 dchrf
 |-  ( ( N e. NN /\ f e. D ) -> f : ( Base ` ( Z/nZ ` N ) ) --> CC )
56 55 ffnd
 |-  ( ( N e. NN /\ f e. D ) -> f Fn ( Base ` ( Z/nZ ` N ) ) )
57 df-ne
 |-  ( ( f ` x ) =/= 0 <-> -. ( f ` x ) = 0 )
58 fvex
 |-  ( f ` x ) e. _V
59 58 elsn
 |-  ( ( f ` x ) e. { 0 } <-> ( f ` x ) = 0 )
60 57 59 xchbinxr
 |-  ( ( f ` x ) =/= 0 <-> -. ( f ` x ) e. { 0 } )
61 oveq1
 |-  ( z = ( f ` x ) -> ( z ^ ( phi ` N ) ) = ( ( f ` x ) ^ ( phi ` N ) ) )
62 61 oveq1d
 |-  ( z = ( f ` x ) -> ( ( z ^ ( phi ` N ) ) - 1 ) = ( ( ( f ` x ) ^ ( phi ` N ) ) - 1 ) )
63 62 eqeq1d
 |-  ( z = ( f ` x ) -> ( ( ( z ^ ( phi ` N ) ) - 1 ) = 0 <-> ( ( ( f ` x ) ^ ( phi ` N ) ) - 1 ) = 0 ) )
64 simpl
 |-  ( ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) -> x e. ( Base ` ( Z/nZ ` N ) ) )
65 ffvelrn
 |-  ( ( f : ( Base ` ( Z/nZ ` N ) ) --> CC /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( f ` x ) e. CC )
66 55 64 65 syl2an
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` x ) e. CC )
67 1 49 2 dchrmhm
 |-  D C_ ( ( mulGrp ` ( Z/nZ ` N ) ) MndHom ( mulGrp ` CCfld ) )
68 simplr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> f e. D )
69 67 68 sselid
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> f e. ( ( mulGrp ` ( Z/nZ ` N ) ) MndHom ( mulGrp ` CCfld ) ) )
70 16 ad2antrr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( phi ` N ) e. NN0 )
71 simprl
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> x e. ( Base ` ( Z/nZ ` N ) ) )
72 eqid
 |-  ( mulGrp ` ( Z/nZ ` N ) ) = ( mulGrp ` ( Z/nZ ` N ) )
73 72 50 mgpbas
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( mulGrp ` ( Z/nZ ` N ) ) )
74 eqid
 |-  ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) = ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) )
75 eqid
 |-  ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
76 73 74 75 mhmmulg
 |-  ( ( f e. ( ( mulGrp ` ( Z/nZ ` N ) ) MndHom ( mulGrp ` CCfld ) ) /\ ( phi ` N ) e. NN0 /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( f ` ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) ) = ( ( phi ` N ) ( .g ` ( mulGrp ` CCfld ) ) ( f ` x ) ) )
77 69 70 71 76 syl3anc
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) ) = ( ( phi ` N ) ( .g ` ( mulGrp ` CCfld ) ) ( f ` x ) ) )
78 nnnn0
 |-  ( N e. NN -> N e. NN0 )
79 49 zncrng
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
80 78 79 syl
 |-  ( N e. NN -> ( Z/nZ ` N ) e. CRing )
81 crngring
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Z/nZ ` N ) e. Ring )
82 80 81 syl
 |-  ( N e. NN -> ( Z/nZ ` N ) e. Ring )
83 82 ad2antrr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( Z/nZ ` N ) e. Ring )
84 eqid
 |-  ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) )
85 eqid
 |-  ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) = ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) )
86 84 85 unitgrp
 |-  ( ( Z/nZ ` N ) e. Ring -> ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) e. Grp )
87 83 86 syl
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) e. Grp )
88 49 84 znunithash
 |-  ( N e. NN -> ( # ` ( Unit ` ( Z/nZ ` N ) ) ) = ( phi ` N ) )
89 88 16 eqeltrd
 |-  ( N e. NN -> ( # ` ( Unit ` ( Z/nZ ` N ) ) ) e. NN0 )
90 fvex
 |-  ( Unit ` ( Z/nZ ` N ) ) e. _V
91 hashclb
 |-  ( ( Unit ` ( Z/nZ ` N ) ) e. _V -> ( ( Unit ` ( Z/nZ ` N ) ) e. Fin <-> ( # ` ( Unit ` ( Z/nZ ` N ) ) ) e. NN0 ) )
92 90 91 ax-mp
 |-  ( ( Unit ` ( Z/nZ ` N ) ) e. Fin <-> ( # ` ( Unit ` ( Z/nZ ` N ) ) ) e. NN0 )
93 89 92 sylibr
 |-  ( N e. NN -> ( Unit ` ( Z/nZ ` N ) ) e. Fin )
94 93 ad2antrr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( Unit ` ( Z/nZ ` N ) ) e. Fin )
95 simprr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` x ) =/= 0 )
96 1 49 2 50 84 68 71 dchrn0
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( f ` x ) =/= 0 <-> x e. ( Unit ` ( Z/nZ ` N ) ) ) )
97 95 96 mpbid
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> x e. ( Unit ` ( Z/nZ ` N ) ) )
98 84 85 unitgrpbas
 |-  ( Unit ` ( Z/nZ ` N ) ) = ( Base ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) )
99 eqid
 |-  ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) = ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) )
100 98 99 oddvds2
 |-  ( ( ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) e. Grp /\ ( Unit ` ( Z/nZ ` N ) ) e. Fin /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ` x ) || ( # ` ( Unit ` ( Z/nZ ` N ) ) ) )
101 87 94 97 100 syl3anc
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ` x ) || ( # ` ( Unit ` ( Z/nZ ` N ) ) ) )
102 88 ad2antrr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( # ` ( Unit ` ( Z/nZ ` N ) ) ) = ( phi ` N ) )
103 101 102 breqtrd
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ` x ) || ( phi ` N ) )
104 15 ad2antrr
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( phi ` N ) e. NN )
105 104 nnzd
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( phi ` N ) e. ZZ )
106 eqid
 |-  ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) = ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) )
107 eqid
 |-  ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) )
108 98 99 106 107 oddvds
 |-  ( ( ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) e. Grp /\ x e. ( Unit ` ( Z/nZ ` N ) ) /\ ( phi ` N ) e. ZZ ) -> ( ( ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ` x ) || ( phi ` N ) <-> ( ( phi ` N ) ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) x ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ) )
109 87 97 105 108 syl3anc
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( ( od ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ` x ) || ( phi ` N ) <-> ( ( phi ` N ) ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) x ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) ) )
110 103 109 mpbid
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( phi ` N ) ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) x ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) )
111 84 72 unitsubm
 |-  ( ( Z/nZ ` N ) e. Ring -> ( Unit ` ( Z/nZ ` N ) ) e. ( SubMnd ` ( mulGrp ` ( Z/nZ ` N ) ) ) )
112 83 111 syl
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( Unit ` ( Z/nZ ` N ) ) e. ( SubMnd ` ( mulGrp ` ( Z/nZ ` N ) ) ) )
113 74 85 106 submmulg
 |-  ( ( ( Unit ` ( Z/nZ ` N ) ) e. ( SubMnd ` ( mulGrp ` ( Z/nZ ` N ) ) ) /\ ( phi ` N ) e. NN0 /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) = ( ( phi ` N ) ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) x ) )
114 112 70 97 113 syl3anc
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) = ( ( phi ` N ) ( .g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) x ) )
115 eqid
 |-  ( 1r ` ( Z/nZ ` N ) ) = ( 1r ` ( Z/nZ ` N ) )
116 72 115 ringidval
 |-  ( 1r ` ( Z/nZ ` N ) ) = ( 0g ` ( mulGrp ` ( Z/nZ ` N ) ) )
117 85 116 subm0
 |-  ( ( Unit ` ( Z/nZ ` N ) ) e. ( SubMnd ` ( mulGrp ` ( Z/nZ ` N ) ) ) -> ( 1r ` ( Z/nZ ` N ) ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) )
118 112 117 syl
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( 1r ` ( Z/nZ ` N ) ) = ( 0g ` ( ( mulGrp ` ( Z/nZ ` N ) ) |`s ( Unit ` ( Z/nZ ` N ) ) ) ) )
119 110 114 118 3eqtr4d
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) = ( 1r ` ( Z/nZ ` N ) ) )
120 119 fveq2d
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` ( ( phi ` N ) ( .g ` ( mulGrp ` ( Z/nZ ` N ) ) ) x ) ) = ( f ` ( 1r ` ( Z/nZ ` N ) ) ) )
121 77 120 eqtr3d
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` CCfld ) ) ( f ` x ) ) = ( f ` ( 1r ` ( Z/nZ ` N ) ) ) )
122 cnfldexp
 |-  ( ( ( f ` x ) e. CC /\ ( phi ` N ) e. NN0 ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` CCfld ) ) ( f ` x ) ) = ( ( f ` x ) ^ ( phi ` N ) ) )
123 66 70 122 syl2anc
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( phi ` N ) ( .g ` ( mulGrp ` CCfld ) ) ( f ` x ) ) = ( ( f ` x ) ^ ( phi ` N ) ) )
124 eqid
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
125 cnfld1
 |-  1 = ( 1r ` CCfld )
126 124 125 ringidval
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
127 116 126 mhm0
 |-  ( f e. ( ( mulGrp ` ( Z/nZ ` N ) ) MndHom ( mulGrp ` CCfld ) ) -> ( f ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 )
128 69 127 syl
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 )
129 121 123 128 3eqtr3d
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( f ` x ) ^ ( phi ` N ) ) = 1 )
130 129 oveq1d
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( ( f ` x ) ^ ( phi ` N ) ) - 1 ) = ( 1 - 1 ) )
131 1m1e0
 |-  ( 1 - 1 ) = 0
132 130 131 eqtrdi
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( ( ( f ` x ) ^ ( phi ` N ) ) - 1 ) = 0 )
133 63 66 132 elrabd
 |-  ( ( ( N e. NN /\ f e. D ) /\ ( x e. ( Base ` ( Z/nZ ` N ) ) /\ ( f ` x ) =/= 0 ) ) -> ( f ` x ) e. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } )
134 133 expr
 |-  ( ( ( N e. NN /\ f e. D ) /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( f ` x ) =/= 0 -> ( f ` x ) e. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
135 60 134 syl5bir
 |-  ( ( ( N e. NN /\ f e. D ) /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( -. ( f ` x ) e. { 0 } -> ( f ` x ) e. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
136 135 orrd
 |-  ( ( ( N e. NN /\ f e. D ) /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( f ` x ) e. { 0 } \/ ( f ` x ) e. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
137 elun
 |-  ( ( f ` x ) e. ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) <-> ( ( f ` x ) e. { 0 } \/ ( f ` x ) e. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
138 136 137 sylibr
 |-  ( ( ( N e. NN /\ f e. D ) /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( f ` x ) e. ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
139 138 ralrimiva
 |-  ( ( N e. NN /\ f e. D ) -> A. x e. ( Base ` ( Z/nZ ` N ) ) ( f ` x ) e. ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
140 ffnfv
 |-  ( f : ( Base ` ( Z/nZ ` N ) ) --> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) <-> ( f Fn ( Base ` ( Z/nZ ` N ) ) /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( f ` x ) e. ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ) )
141 56 139 140 sylanbrc
 |-  ( ( N e. NN /\ f e. D ) -> f : ( Base ` ( Z/nZ ` N ) ) --> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) )
142 141 ex
 |-  ( N e. NN -> ( f e. D -> f : ( Base ` ( Z/nZ ` N ) ) --> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ) )
143 48 51 elmapd
 |-  ( N e. NN -> ( f e. ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ^m ( Base ` ( Z/nZ ` N ) ) ) <-> f : ( Base ` ( Z/nZ ` N ) ) --> ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ) )
144 142 143 sylibrd
 |-  ( N e. NN -> ( f e. D -> f e. ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ^m ( Base ` ( Z/nZ ` N ) ) ) ) )
145 144 ssrdv
 |-  ( N e. NN -> D C_ ( ( { 0 } u. { z e. CC | ( ( z ^ ( phi ` N ) ) - 1 ) = 0 } ) ^m ( Base ` ( Z/nZ ` N ) ) ) )
146 53 145 ssfid
 |-  ( N e. NN -> D e. Fin )