This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrfi.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion dchrfi ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )

Proof

Step Hyp Ref Expression
1 dchrabl.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrfi.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 snfi ⊢ { 0 } ∈ Fin
4 cnex ⊢ ℂ ∈ V
5 4 a1i ⊢ ( 𝑁 ∈ ℕ → ℂ ∈ V )
6 ovexd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ∈ V )
7 1cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ ) → 1 ∈ ℂ )
8 eqidd ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) )
9 fconstmpt ⊢ ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 )
10 9 a1i ⊢ ( 𝑁 ∈ ℕ → ( ℂ × { 1 } ) = ( 𝑧 ∈ ℂ ↦ 1 ) )
11 5 6 7 8 10 offval2 ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∘f − ( ℂ × { 1 } ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) )
12 ssid ⊢ ℂ ⊆ ℂ
13 12 a1i ⊢ ( 𝑁 ∈ ℕ → ℂ ⊆ ℂ )
14 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
15 phicl ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )
16 15 nnnn0d ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
17 plypow ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∈ ( Poly ‘ ℂ ) )
18 13 14 16 17 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∈ ( Poly ‘ ℂ ) )
19 ax-1cn ⊢ 1 ∈ ℂ
20 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) )
21 12 19 20 mp2an ⊢ ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ )
22 plysubcl ⊢ ( ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 1 } ) ∈ ( Poly ‘ ℂ ) ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∘f − ( ℂ × { 1 } ) ) ∈ ( Poly ‘ ℂ ) )
23 18 21 22 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) ) ∘f − ( ℂ × { 1 } ) ) ∈ ( Poly ‘ ℂ ) )
24 11 23 eqeltrrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∈ ( Poly ‘ ℂ ) )
25 0cn ⊢ 0 ∈ ℂ
26 neg1ne0 ⊢ - 1 ≠ 0
27 15 0expd ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ ( ϕ ‘ 𝑁 ) ) = 0 )
28 27 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = ( 0 − 1 ) )
29 oveq1 ⊢ ( 𝑧 = 0 → ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) = ( 0 ↑ ( ϕ ‘ 𝑁 ) ) )
30 29 oveq1d ⊢ ( 𝑧 = 0 → ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = ( ( 0 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
31 eqid ⊢ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
32 ovex ⊢ ( ( 0 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ∈ V
33 30 31 32 fvmpt ⊢ ( 0 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) = ( ( 0 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
34 25 33 ax-mp ⊢ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) = ( ( 0 ↑ ( ϕ ‘ 𝑁 ) ) − 1 )
35 df-neg ⊢ - 1 = ( 0 − 1 )
36 28 34 35 3eqtr4g ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) = - 1 )
37 36 neeq1d ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) ≠ 0 ↔ - 1 ≠ 0 ) )
38 26 37 mpbiri ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) ≠ 0 )
39 ne0p ⊢ ( ( 0 ∈ ℂ ∧ ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ‘ 0 ) ≠ 0 ) → ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ≠ 0𝑝 )
40 25 38 39 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ≠ 0𝑝 )
41 31 mptiniseg ⊢ ( 0 ∈ ℂ → ( ◡ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) “ { 0 } ) = { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } )
42 25 41 ax-mp ⊢ ( ◡ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) “ { 0 } ) = { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 }
43 42 eqcomi ⊢ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } = ( ◡ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) “ { 0 } )
44 43 fta1 ⊢ ( ( ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ≠ 0𝑝 ) → ( { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ∈ Fin ∧ ( ♯ ‘ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ≤ ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ) ) )
45 24 40 44 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ∈ Fin ∧ ( ♯ ‘ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ≤ ( deg ‘ ( 𝑧 ∈ ℂ ↦ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) ) ) ) )
46 45 simpld ⊢ ( 𝑁 ∈ ℕ → { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ∈ Fin )
47 unfi ⊢ ( ( { 0 } ∈ Fin ∧ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ∈ Fin ) → ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ∈ Fin )
48 3 46 47 sylancr ⊢ ( 𝑁 ∈ ℕ → ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ∈ Fin )
49 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
50 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) )
51 49 50 znfi ⊢ ( 𝑁 ∈ ℕ → ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin )
52 mapfi ⊢ ( ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ∈ Fin ∧ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ) → ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↑m ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Fin )
53 48 51 52 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↑m ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Fin )
54 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ 𝐷 )
55 1 49 2 50 54 dchrf ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ )
56 55 ffnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) → 𝑓 Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
57 df-ne ⊢ ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑓 ‘ 𝑥 ) = 0 )
58 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
59 58 elsn ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝑓 ‘ 𝑥 ) = 0 )
60 57 59 xchbinxr ⊢ ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ ¬ ( 𝑓 ‘ 𝑥 ) ∈ { 0 } )
61 oveq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑥 ) → ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) = ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) )
62 61 oveq1d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = ( ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) )
63 62 eqeq1d ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑥 ) → ( ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 ↔ ( ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 ) )
64 simpl ⊢ ( ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) → 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
65 ffvelcdm ⊢ ( ( 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
66 55 64 65 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
67 1 49 2 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) MndHom ( mulGrp ‘ ℂfld ) )
68 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → 𝑓 ∈ 𝐷 )
69 67 68 sselid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → 𝑓 ∈ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) MndHom ( mulGrp ‘ ℂfld ) ) )
70 16 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
71 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
72 eqid ⊢ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) )
73 72 50 mgpbas ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
74 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
75 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
76 73 74 75 mhmmulg ⊢ ( ( 𝑓 ∈ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑓 ‘ ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) ) = ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑓 ‘ 𝑥 ) ) )
77 69 70 71 76 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) ) = ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑓 ‘ 𝑥 ) ) )
78 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
79 49 zncrng ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
80 78 79 syl ⊢ ( 𝑁 ∈ ℕ → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
81 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
82 80 81 syl ⊢ ( 𝑁 ∈ ℕ → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
83 82 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
84 eqid ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) )
85 eqid ⊢ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
86 84 85 unitgrp ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring → ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Grp )
87 83 86 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Grp )
88 49 84 znunithash ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ϕ ‘ 𝑁 ) )
89 88 16 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ℕ0 )
90 fvex ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V
91 hashclb ⊢ ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ V → ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ↔ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ℕ0 ) )
92 90 91 ax-mp ⊢ ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ↔ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ℕ0 )
93 89 92 sylibr ⊢ ( 𝑁 ∈ ℕ → ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin )
94 93 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin )
95 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ 𝑥 ) ≠ 0 )
96 1 49 2 50 84 68 71 dchrn0 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) ≠ 0 ↔ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
97 95 96 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
98 84 85 unitgrpbas ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Base ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
99 eqid ⊢ ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
100 98 99 oddvds2 ⊢ ( ( ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Grp ∧ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Fin ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ‘ 𝑥 ) ∥ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
101 87 94 97 100 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ‘ 𝑥 ) ∥ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
102 88 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ϕ ‘ 𝑁 ) )
103 101 102 breqtrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ‘ 𝑥 ) ∥ ( ϕ ‘ 𝑁 ) )
104 15 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
105 104 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ϕ ‘ 𝑁 ) ∈ ℤ )
106 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
107 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
108 98 99 106 107 oddvds ⊢ ( ( ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Grp ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( ϕ ‘ 𝑁 ) ∈ ℤ ) → ( ( ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ‘ 𝑥 ) ∥ ( ϕ ‘ 𝑁 ) ↔ ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) 𝑥 ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ) )
109 87 97 105 108 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( od ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ‘ 𝑥 ) ∥ ( ϕ ‘ 𝑁 ) ↔ ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) 𝑥 ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ) )
110 103 109 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) 𝑥 ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
111 84 72 unitsubm ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring → ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
112 83 111 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
113 74 85 106 submmulg ⊢ ( ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ∧ 𝑥 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) = ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) 𝑥 ) )
114 112 70 97 113 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) = ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) 𝑥 ) )
115 eqid ⊢ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) )
116 72 115 ringidval ⊢ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 0g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
117 85 116 subm0 ⊢ ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
118 112 117 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( 0g ‘ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↾s ( Unit ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
119 110 114 118 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) = ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
120 119 fveq2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) 𝑥 ) ) = ( 𝑓 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
121 77 120 eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑓 ‘ 𝑥 ) ) = ( 𝑓 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
122 cnfldexp ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ℂ ∧ ( ϕ ‘ 𝑁 ) ∈ ℕ0 ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) )
123 66 70 122 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ϕ ‘ 𝑁 ) ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( 𝑓 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) )
124 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
125 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
126 124 125 ringidval ⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
127 116 126 mhm0 ⊢ ( 𝑓 ∈ ( ( mulGrp ‘ ( ℤ/nℤ ‘ 𝑁 ) ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑓 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 )
128 69 127 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ ( 1r ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = 1 )
129 121 123 128 3eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) = 1 )
130 129 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = ( 1 − 1 ) )
131 1m1e0 ⊢ ( 1 − 1 ) = 0
132 130 131 eqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( 𝑓 ‘ 𝑥 ) ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 )
133 63 66 132 elrabd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ( 𝑓 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } )
134 133 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ≠ 0 → ( 𝑓 ‘ 𝑥 ) ∈ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
135 60 134 biimtrrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ¬ ( 𝑓 ‘ 𝑥 ) ∈ { 0 } → ( 𝑓 ‘ 𝑥 ) ∈ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
136 135 orrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ { 0 } ∨ ( 𝑓 ‘ 𝑥 ) ∈ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
137 elun ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ { 0 } ∨ ( 𝑓 ‘ 𝑥 ) ∈ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
138 136 137 sylibr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
139 138 ralrimiva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) → ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑓 ‘ 𝑥 ) ∈ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
140 ffnfv ⊢ ( 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↔ ( 𝑓 Fn ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( 𝑓 ‘ 𝑥 ) ∈ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ) )
141 56 139 140 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) → 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) )
142 141 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑓 ∈ 𝐷 → 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ) )
143 48 51 elmapd ⊢ ( 𝑁 ∈ ℕ → ( 𝑓 ∈ ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↑m ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↔ 𝑓 : ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ⟶ ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ) )
144 142 143 sylibrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑓 ∈ 𝐷 → 𝑓 ∈ ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↑m ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
145 144 ssrdv ⊢ ( 𝑁 ∈ ℕ → 𝐷 ⊆ ( ( { 0 } ∪ { 𝑧 ∈ ℂ ∣ ( ( 𝑧 ↑ ( ϕ ‘ 𝑁 ) ) − 1 ) = 0 } ) ↑m ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
146 53 145 ssfid ⊢ ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )