Step | Hyp | Ref
| Expression |
1 | | znf1o.y |
. . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
2 | 1 | zncrng 19893 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
3 | | crngring 18558 |
. . . . . 6
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
4 | | eqid 2622 |
. . . . . . 7
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
5 | 4 | zrhrhm 19860 |
. . . . . 6
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
6 | | zringbas 19824 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
7 | | znf1o.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
8 | 6, 7 | rhmf 18726 |
. . . . . 6
⊢
((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) →
(ℤRHom‘𝑌):ℤ⟶𝐵) |
9 | 2, 3, 5, 8 | 4syl 19 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ⟶𝐵) |
10 | | znf1o.w |
. . . . . 6
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
11 | | sseq1 3626 |
. . . . . . 7
⊢ (ℤ
= if(𝑁 = 0, ℤ,
(0..^𝑁)) → (ℤ
⊆ ℤ ↔ if(𝑁
= 0, ℤ, (0..^𝑁))
⊆ ℤ)) |
12 | | sseq1 3626 |
. . . . . . 7
⊢
((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔
if(𝑁 = 0, ℤ,
(0..^𝑁)) ⊆
ℤ)) |
13 | | ssid 3624 |
. . . . . . 7
⊢ ℤ
⊆ ℤ |
14 | | elfzoelz 12470 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
15 | 14 | ssriv 3607 |
. . . . . . 7
⊢
(0..^𝑁) ⊆
ℤ |
16 | 11, 12, 13, 15 | keephyp 4152 |
. . . . . 6
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆
ℤ |
17 | 10, 16 | eqsstri 3635 |
. . . . 5
⊢ 𝑊 ⊆
ℤ |
18 | | fssres 6070 |
. . . . 5
⊢
(((ℤRHom‘𝑌):ℤ⟶𝐵 ∧ 𝑊 ⊆ ℤ) →
((ℤRHom‘𝑌)
↾ 𝑊):𝑊⟶𝐵) |
19 | 9, 17, 18 | sylancl 694 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) |
20 | | znf1o.f |
. . . . 5
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) |
21 | 20 | feq1i 6036 |
. . . 4
⊢ (𝐹:𝑊⟶𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) |
22 | 19, 21 | sylibr 224 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊⟶𝐵) |
23 | 20 | fveq1i 6192 |
. . . . . . . 8
⊢ (𝐹‘𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) |
24 | | fvres 6207 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
25 | 24 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
26 | 23, 25 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
27 | 20 | fveq1i 6192 |
. . . . . . . 8
⊢ (𝐹‘𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) |
28 | | fvres 6207 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
29 | 28 | ad2antll 765 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
30 | 27, 29 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
31 | 26, 30 | eqeq12d 2637 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦))) |
32 | | simpl 473 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℕ0) |
33 | | simprl 794 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) |
34 | 17, 33 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
35 | | simprr 796 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) |
36 | 17, 35 | sseldi 3601 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
37 | 1, 4 | zndvds 19898 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ
∧ 𝑦 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
38 | 32, 34, 36, 37 | syl3anc 1326 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
39 | | elnn0 11294 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
40 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℕ) |
41 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) |
42 | 17, 41 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
43 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) |
44 | 17, 43 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
45 | | moddvds 14991 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
46 | 40, 42, 44, 45 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
47 | 42 | zred 11482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℝ) |
48 | | nnrp 11842 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
49 | 48 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℝ+) |
50 | | nnne0 11053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
51 | | ifnefalse 4098 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
53 | 10, 52 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑊 = (0..^𝑁)) |
55 | 41, 54 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ (0..^𝑁)) |
56 | | elfzole1 12478 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑥) |
58 | | elfzolt2 12479 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁) |
59 | 55, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 < 𝑁) |
60 | | modid 12695 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥) |
61 | 47, 49, 57, 59, 60 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 mod 𝑁) = 𝑥) |
62 | 44 | zred 11482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℝ) |
63 | 43, 54 | eleqtrd 2703 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ (0..^𝑁)) |
64 | | elfzole1 12478 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑦) |
66 | | elfzolt2 12479 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁) |
67 | 63, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 < 𝑁) |
68 | | modid 12695 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦) |
69 | 62, 49, 65, 67, 68 | syl22anc 1327 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑦 mod 𝑁) = 𝑦) |
70 | 61, 69 | eqeq12d 2637 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦)) |
71 | 46, 70 | bitr3d 270 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
72 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 = 0) |
73 | 72 | breq1d 4663 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 0 ∥ (𝑥 − 𝑦))) |
74 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → 𝑁 = 0) |
75 | | 0nn0 11307 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
76 | 74, 75 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → 𝑁 ∈
ℕ0) |
77 | 76, 34 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
78 | 76, 36 | sylan 488 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
79 | 77, 78 | zsubcld 11487 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 − 𝑦) ∈ ℤ) |
80 | | 0dvds 15002 |
. . . . . . . . . 10
⊢ ((𝑥 − 𝑦) ∈ ℤ → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) |
81 | 79, 80 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) |
82 | 77 | zcnd 11483 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℂ) |
83 | 78 | zcnd 11483 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℂ) |
84 | 82, 83 | subeq0ad 10402 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) |
85 | 73, 81, 84 | 3bitrd 294 |
. . . . . . . 8
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
86 | 71, 85 | jaoian 824 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
87 | 39, 86 | sylanb 489 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
88 | 31, 38, 87 | 3bitrd 294 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
89 | 88 | biimpd 219 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
90 | 89 | ralrimivva 2971 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
91 | | dff13 6512 |
. . 3
⊢ (𝐹:𝑊–1-1→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
92 | 22, 90, 91 | sylanbrc 698 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1→𝐵) |
93 | | zmodfzo 12693 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) |
94 | 93 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) |
95 | 53 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁)) |
96 | 94, 95 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊) |
97 | | zre 11381 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
98 | | modabs2 12704 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) |
99 | 97, 48, 98 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) |
100 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ) |
101 | 15, 94 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ) |
102 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℤ) |
103 | | moddvds 14991 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
104 | 100, 101,
102, 103 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
105 | 99, 104 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)) |
106 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
107 | 106 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ0) |
108 | 1, 4 | zndvds 19898 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
109 | 107, 101,
102, 108 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
110 | 105, 109 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧)) |
111 | 110 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) |
112 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) |
113 | 112 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑧 mod 𝑁) → (((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))) |
114 | 113 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
115 | 96, 111, 114 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
116 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ) |
117 | 116 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ)) |
118 | 117 | biimpar 502 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁))) |
119 | 118, 10 | syl6eleqr 2712 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ 𝑊) |
120 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) |
121 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧)) |
122 | 121 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧))) |
123 | 122 | rspcev 3309 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
124 | 119, 120,
123 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
125 | 115, 124 | jaoian 824 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
126 | 39, 125 | sylanb 489 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
127 | 27, 28 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
128 | 127 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))) |
129 | 128 | rexbiia 3040 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
130 | 126, 129 | sylibr 224 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) |
131 | 130 | ralrimiva 2966 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ∀𝑧 ∈
ℤ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) |
132 | 1, 7, 4 | znzrhfo 19896 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→𝐵) |
133 | | fofn 6117 |
. . . . . 6
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → (ℤRHom‘𝑌) Fn ℤ) |
134 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
135 | 134 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
136 | 135 | ralrn 6362 |
. . . . . 6
⊢
((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
137 | 132, 133,
136 | 3syl 18 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (∀𝑥 ∈
ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
138 | 131, 137 | mpbird 247 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) |
139 | | forn 6118 |
. . . . . 6
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → ran (ℤRHom‘𝑌) = 𝐵) |
140 | 132, 139 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ran (ℤRHom‘𝑌) = 𝐵) |
141 | 140 | raleqdv 3144 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (∀𝑥 ∈
ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))) |
142 | 138, 141 | mpbid 222 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) |
143 | | dffo3 6374 |
. . 3
⊢ (𝐹:𝑊–onto→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))) |
144 | 22, 142, 143 | sylanbrc 698 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–onto→𝐵) |
145 | | df-f1o 5895 |
. 2
⊢ (𝐹:𝑊–1-1-onto→𝐵 ↔ (𝐹:𝑊–1-1→𝐵 ∧ 𝐹:𝑊–onto→𝐵)) |
146 | 92, 144, 145 | sylanbrc 698 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝐵) |