Step | Hyp | Ref
| Expression |
1 | | znf1o.y |
. . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
2 | 1 | zncrng 20363 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
3 | | crngring 19428 |
. . . . . 6
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
4 | | eqid 2738 |
. . . . . . 7
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) |
5 | 4 | zrhrhm 20332 |
. . . . . 6
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) |
6 | | zringbas 20295 |
. . . . . . 7
⊢ ℤ =
(Base‘ℤring) |
7 | | znf1o.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
8 | 6, 7 | rhmf 19600 |
. . . . . 6
⊢
((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) →
(ℤRHom‘𝑌):ℤ⟶𝐵) |
9 | 2, 3, 5, 8 | 4syl 19 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ⟶𝐵) |
10 | | znf1o.w |
. . . . . 6
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) |
11 | | sseq1 3902 |
. . . . . . 7
⊢ (ℤ
= if(𝑁 = 0, ℤ,
(0..^𝑁)) → (ℤ
⊆ ℤ ↔ if(𝑁
= 0, ℤ, (0..^𝑁))
⊆ ℤ)) |
12 | | sseq1 3902 |
. . . . . . 7
⊢
((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔
if(𝑁 = 0, ℤ,
(0..^𝑁)) ⊆
ℤ)) |
13 | | ssid 3899 |
. . . . . . 7
⊢ ℤ
⊆ ℤ |
14 | | elfzoelz 13129 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
15 | 14 | ssriv 3881 |
. . . . . . 7
⊢
(0..^𝑁) ⊆
ℤ |
16 | 11, 12, 13, 15 | keephyp 4485 |
. . . . . 6
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆
ℤ |
17 | 10, 16 | eqsstri 3911 |
. . . . 5
⊢ 𝑊 ⊆
ℤ |
18 | | fssres 6544 |
. . . . 5
⊢
(((ℤRHom‘𝑌):ℤ⟶𝐵 ∧ 𝑊 ⊆ ℤ) →
((ℤRHom‘𝑌)
↾ 𝑊):𝑊⟶𝐵) |
19 | 9, 17, 18 | sylancl 589 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) |
20 | | znf1o.f |
. . . . 5
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) |
21 | 20 | feq1i 6495 |
. . . 4
⊢ (𝐹:𝑊⟶𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) |
22 | 19, 21 | sylibr 237 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊⟶𝐵) |
23 | 20 | fveq1i 6675 |
. . . . . . . 8
⊢ (𝐹‘𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) |
24 | | fvres 6693 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
25 | 24 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
26 | 23, 25 | syl5eq 2785 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) |
27 | 20 | fveq1i 6675 |
. . . . . . . 8
⊢ (𝐹‘𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) |
28 | | fvres 6693 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
29 | 28 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
30 | 27, 29 | syl5eq 2785 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
31 | 26, 30 | eqeq12d 2754 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦))) |
32 | | simpl 486 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℕ0) |
33 | | simprl 771 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) |
34 | 17, 33 | sseldi 3875 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
35 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) |
36 | 17, 35 | sseldi 3875 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
37 | 1, 4 | zndvds 20368 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ
∧ 𝑦 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
38 | 32, 34, 36, 37 | syl3anc 1372 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
39 | | elnn0 11978 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
40 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℕ) |
41 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) |
42 | 17, 41 | sseldi 3875 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
43 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) |
44 | 17, 43 | sseldi 3875 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
45 | | moddvds 15710 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
46 | 40, 42, 44, 45 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) |
47 | 42 | zred 12168 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℝ) |
48 | | nnrp 12483 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
49 | 48 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℝ+) |
50 | | nnne0 11750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
51 | | ifnefalse 4426 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
53 | 10, 52 | syl5eq 2785 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁)) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑊 = (0..^𝑁)) |
55 | 41, 54 | eleqtrd 2835 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ (0..^𝑁)) |
56 | | elfzole1 13137 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑥) |
58 | | elfzolt2 13138 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁) |
59 | 55, 58 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 < 𝑁) |
60 | | modid 13355 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥) |
61 | 47, 49, 57, 59, 60 | syl22anc 838 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 mod 𝑁) = 𝑥) |
62 | 44 | zred 12168 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℝ) |
63 | 43, 54 | eleqtrd 2835 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ (0..^𝑁)) |
64 | | elfzole1 13137 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑦) |
66 | | elfzolt2 13138 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁) |
67 | 63, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 < 𝑁) |
68 | | modid 13355 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦) |
69 | 62, 49, 65, 67, 68 | syl22anc 838 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑦 mod 𝑁) = 𝑦) |
70 | 61, 69 | eqeq12d 2754 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦)) |
71 | 46, 70 | bitr3d 284 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
72 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 = 0) |
73 | 72 | breq1d 5040 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 0 ∥ (𝑥 − 𝑦))) |
74 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → 𝑁 = 0) |
75 | | 0nn0 11991 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
76 | 74, 75 | eqeltrdi 2841 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → 𝑁 ∈
ℕ0) |
77 | 76, 34 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) |
78 | 76, 36 | sylan 583 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) |
79 | 77, 78 | zsubcld 12173 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 − 𝑦) ∈ ℤ) |
80 | | 0dvds 15722 |
. . . . . . . . . 10
⊢ ((𝑥 − 𝑦) ∈ ℤ → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) |
81 | 79, 80 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) |
82 | 77 | zcnd 12169 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℂ) |
83 | 78 | zcnd 12169 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℂ) |
84 | 82, 83 | subeq0ad 11085 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) |
85 | 73, 81, 84 | 3bitrd 308 |
. . . . . . . 8
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
86 | 71, 85 | jaoian 956 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
87 | 39, 86 | sylanb 584 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) |
88 | 31, 38, 87 | 3bitrd 308 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦)) |
89 | 88 | biimpd 232 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
90 | 89 | ralrimivva 3103 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
91 | | dff13 7024 |
. . 3
⊢ (𝐹:𝑊–1-1→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
92 | 22, 90, 91 | sylanbrc 586 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1→𝐵) |
93 | | zmodfzo 13353 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) |
94 | 93 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) |
95 | 53 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁)) |
96 | 94, 95 | eleqtrrd 2836 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊) |
97 | | zre 12066 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
98 | | modabs2 13364 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) |
99 | 97, 48, 98 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) |
100 | | simpl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ) |
101 | 15, 94 | sseldi 3875 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ) |
102 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℤ) |
103 | | moddvds 15710 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
104 | 100, 101,
102, 103 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
105 | 99, 104 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)) |
106 | | nnnn0 11983 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
107 | 106 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ0) |
108 | 1, 4 | zndvds 20368 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
109 | 107, 101,
102, 108 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) |
110 | 105, 109 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧)) |
111 | 110 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) |
112 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) |
113 | 112 | rspceeqv 3541 |
. . . . . . . . . 10
⊢ (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
114 | 96, 111, 113 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
115 | | iftrue 4420 |
. . . . . . . . . . . . 13
⊢ (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ) |
116 | 115 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ)) |
117 | 116 | biimpar 481 |
. . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁))) |
118 | 117, 10 | eleqtrrdi 2844 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ 𝑊) |
119 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) |
120 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧)) |
121 | 120 | rspceeqv 3541 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
122 | 118, 119,
121 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
123 | 114, 122 | jaoian 956 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
124 | 39, 123 | sylanb 584 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
125 | 27, 28 | syl5eq 2785 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) |
126 | 125 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))) |
127 | 126 | rexbiia 3160 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) |
128 | 124, 127 | sylibr 237 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) |
129 | 128 | ralrimiva 3096 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ∀𝑧 ∈
ℤ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) |
130 | 1, 7, 4 | znzrhfo 20366 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→𝐵) |
131 | | fofn 6594 |
. . . . . 6
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → (ℤRHom‘𝑌) Fn ℤ) |
132 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
133 | 132 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
134 | 133 | ralrn 6864 |
. . . . . 6
⊢
((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
135 | 130, 131,
134 | 3syl 18 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (∀𝑥 ∈
ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) |
136 | 129, 135 | mpbird 260 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) |
137 | | forn 6595 |
. . . . . 6
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → ran (ℤRHom‘𝑌) = 𝐵) |
138 | 130, 137 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ran (ℤRHom‘𝑌) = 𝐵) |
139 | 138 | raleqdv 3316 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (∀𝑥 ∈
ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))) |
140 | 136, 139 | mpbid 235 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) |
141 | | dffo3 6878 |
. . 3
⊢ (𝐹:𝑊–onto→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))) |
142 | 22, 140, 141 | sylanbrc 586 |
. 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–onto→𝐵) |
143 | | df-f1o 6346 |
. 2
⊢ (𝐹:𝑊–1-1-onto→𝐵 ↔ (𝐹:𝑊–1-1→𝐵 ∧ 𝐹:𝑊–onto→𝐵)) |
144 | 92, 142, 143 | sylanbrc 586 |
1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝐵) |