Step | Hyp | Ref
| Expression |
1 | | snfi 8834 |
. . . 4
⊢ {0}
∈ Fin |
2 | | cnex 10952 |
. . . . . . . . 9
⊢ ℂ
∈ V |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ℂ
∈ V) |
4 | | ovexd 7310 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → (𝑧↑(ϕ‘𝑁)) ∈ V) |
5 | | 1cnd 10970 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
6 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) = (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁)))) |
7 | | fconstmpt 5649 |
. . . . . . . . 9
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1)) |
9 | 3, 4, 5, 6, 8 | offval2 7553 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) = (𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))) |
10 | | ssid 3943 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ℂ
⊆ ℂ) |
12 | | 1cnd 10970 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
13 | | phicl 16470 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ) |
14 | 13 | nnnn0d 12293 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ0) |
15 | | plypow 25366 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
16 | 11, 12, 14, 15 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
17 | | ax-1cn 10929 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
18 | | plyconst 25367 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → (ℂ × {1}) ∈
(Poly‘ℂ)) |
19 | 10, 17, 18 | mp2an 689 |
. . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℂ) |
20 | | plysubcl 25383 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ)
∧ (ℂ × {1}) ∈ (Poly‘ℂ)) → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) ∈ (Poly‘ℂ)) |
21 | 16, 19, 20 | sylancl 586 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) ∈ (Poly‘ℂ)) |
22 | 9, 21 | eqeltrrd 2840 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ)) |
23 | | 0cn 10967 |
. . . . . . 7
⊢ 0 ∈
ℂ |
24 | | neg1ne0 12089 |
. . . . . . . 8
⊢ -1 ≠
0 |
25 | 13 | 0expd 13857 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0↑(ϕ‘𝑁)) =
0) |
26 | 25 | oveq1d 7290 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((0↑(ϕ‘𝑁))
− 1) = (0 − 1)) |
27 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧↑(ϕ‘𝑁)) = (0↑(ϕ‘𝑁))) |
28 | 27 | oveq1d 7290 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝑧↑(ϕ‘𝑁)) − 1) = ((0↑(ϕ‘𝑁)) − 1)) |
29 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) |
30 | | ovex 7308 |
. . . . . . . . . . . 12
⊢
((0↑(ϕ‘𝑁)) − 1) ∈ V |
31 | 28, 29, 30 | fvmpt 6875 |
. . . . . . . . . . 11
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1)) |
32 | 23, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1) |
33 | | df-neg 11208 |
. . . . . . . . . 10
⊢ -1 = (0
− 1) |
34 | 26, 32, 33 | 3eqtr4g 2803 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
-1) |
35 | 34 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0
↔ -1 ≠ 0)) |
36 | 24, 35 | mpbiri 257 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠
0) |
37 | | ne0p 25368 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0) →
(𝑧 ∈ ℂ ↦
((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
38 | 23, 36, 37 | sylancr 587 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
39 | 29 | mptiniseg 6142 |
. . . . . . . . 9
⊢ (0 ∈
ℂ → (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}) |
40 | 23, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0} |
41 | 40 | eqcomi 2747 |
. . . . . . 7
⊢ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} = (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) |
42 | 41 | fta1 25468 |
. . . . . 6
⊢ (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
→ ({𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧
(♯‘{𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
43 | 22, 38, 42 | syl2anc 584 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin
∧ (♯‘{𝑧
∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
44 | 43 | simpld 495 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈
Fin) |
45 | | unfi 8955 |
. . . 4
⊢ (({0}
∈ Fin ∧ {𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin) → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
46 | 1, 44, 45 | sylancr 587 |
. . 3
⊢ (𝑁 ∈ ℕ → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
47 | | eqid 2738 |
. . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) |
48 | | eqid 2738 |
. . . 4
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) |
49 | 47, 48 | znfi 20767 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
50 | | mapfi 9115 |
. . 3
⊢ ((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin ∧
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
51 | 46, 49, 50 | syl2anc 584 |
. 2
⊢ (𝑁 ∈ ℕ → (({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑m
(Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
52 | | dchrabl.g |
. . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) |
53 | | dchrfi.b |
. . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) |
54 | | simpr 485 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
55 | 52, 47, 53, 48, 54 | dchrf 26390 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
56 | 55 | ffnd 6601 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) |
57 | | df-ne 2944 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0) |
58 | | fvex 6787 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
59 | 58 | elsn 4576 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ {0} ↔ (𝑓‘𝑥) = 0) |
60 | 57, 59 | xchbinxr 335 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) ∈ {0}) |
61 | | oveq1 7282 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑓‘𝑥) → (𝑧↑(ϕ‘𝑁)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
62 | 61 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑓‘𝑥) → ((𝑧↑(ϕ‘𝑁)) − 1) = (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1)) |
63 | 62 | eqeq1d 2740 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑓‘𝑥) → (((𝑧↑(ϕ‘𝑁)) − 1) = 0 ↔ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) |
64 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
65 | | ffvelrn 6959 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ℂ) |
66 | 55, 64, 65 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ ℂ) |
67 | 52, 47, 53 | dchrmhm 26389 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) |
68 | | simplr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈ 𝐷) |
69 | 67, 68 | sselid 3919 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld))) |
70 | 14 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ0) |
71 | | simprl 768 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
72 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘(ℤ/nℤ‘𝑁)) =
(mulGrp‘(ℤ/nℤ‘𝑁)) |
73 | 72, 48 | mgpbas 19726 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
74 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) =
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
75 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
76 | 73, 74, 75 | mhmmulg 18744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
77 | 69, 70, 71, 76 | syl3anc 1370 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
78 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
79 | 47 | zncrng 20752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ CRing) |
81 | | crngring 19795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(ℤ/nℤ‘𝑁) ∈ Ring) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ Ring) |
83 | 82 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(ℤ/nℤ‘𝑁) ∈ Ring) |
84 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) |
85 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) =
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) |
86 | 84, 85 | unitgrp 19909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
87 | 83, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
88 | 47, 84 | znunithash 20772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
89 | 88, 14 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
90 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Unit‘(ℤ/nℤ‘𝑁)) ∈ V |
91 | | hashclb 14073 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ V →
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0)) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
93 | 89, 92 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
94 | 93 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
95 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ≠ 0) |
96 | 52, 47, 53, 48, 84, 68, 71 | dchrn0 26398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥) ≠ 0 ↔ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) |
97 | 95, 96 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) |
98 | 84, 85 | unitgrpbas 19908 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Base‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
99 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
100 | 98, 99 | oddvds2 19173 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((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 1370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(♯‘(Unit‘(ℤ/nℤ‘𝑁)))) |
102 | 88 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
103 | 101, 102 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁)) |
104 | 13 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ) |
105 | 104 | nnzd 12425 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℤ) |
106 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
107 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
108 | 98, 99, 106, 107 | oddvds 19155 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((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 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(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 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))) |
111 | 84, 72 | unitsubm 19912 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
112 | 83, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
113 | 74, 85, 106 | submmulg 18747 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
114 | 112, 70, 97, 113 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
115 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) |
116 | 72, 115 | ringidval 19739 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
117 | 85, 116 | subm0 18454 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
118 | 112, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
119 | 110, 114,
118 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
(1r‘(ℤ/nℤ‘𝑁))) |
120 | 119 | fveq2d 6778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
(𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
121 | 77, 120 | eqtr3d 2780 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
122 | | cnfldexp 20631 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0)
→ ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
123 | 66, 70, 122 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
124 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
125 | | cnfld1 20623 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(1r‘ℂfld) |
126 | 124, 125 | ringidval 19739 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
127 | 116, 126 | mhm0 18438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
128 | 69, 127 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
129 | 121, 123,
128 | 3eqtr3d 2786 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥)↑(ϕ‘𝑁)) = 1) |
130 | 129 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = (1 −
1)) |
131 | | 1m1e0 12045 |
. . . . . . . . . . . . 13
⊢ (1
− 1) = 0 |
132 | 130, 131 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0) |
133 | 63, 66, 132 | elrabd 3626 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) |
134 | 133 | expr 457 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ≠ 0 → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
135 | 60, 134 | syl5bir 242 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (¬ (𝑓‘𝑥) ∈ {0} → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
136 | 135 | orrd 860 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
137 | | elun 4083 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
138 | 136, 137 | sylibr 233 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
139 | 138 | ralrimiva 3103 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
140 | | ffnfv 6992 |
. . . . . 6
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ (𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))) |
141 | 56, 139, 140 | sylanbrc 583 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0})) |
142 | 141 | ex 413 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
143 | 46, 49 | elmapd 8629 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁))) ↔ 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
144 | 142, 143 | sylibrd 258 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑m
(Base‘(ℤ/nℤ‘𝑁))))) |
145 | 144 | ssrdv 3927 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁)))) |
146 | 51, 145 | ssfid 9042 |
1
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |