| 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 |
|
ffvelrn |
⊢ ( ( 𝑓 : ( 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
|
sseldi |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑥 ∈ ( 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
|
syl5bir |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷 ) ∧ 𝑥 ∈ ( 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 ) |