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 ffvelcdm 
 |-  ( ( 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 biimtrrid 
 |-  ( ( ( 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 )