| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | znf1o.y | . . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) | 
| 2 | 1 | zncrng 21563 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) | 
| 3 |  | crngring 20242 | . . . . . 6
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) | 
| 4 |  | eqid 2737 | . . . . . . 7
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) | 
| 5 | 4 | zrhrhm 21522 | . . . . . 6
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) | 
| 6 |  | zringbas 21464 | . . . . . . 7
⊢ ℤ =
(Base‘ℤring) | 
| 7 |  | znf1o.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑌) | 
| 8 | 6, 7 | rhmf 20485 | . . . . . 6
⊢
((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) →
(ℤRHom‘𝑌):ℤ⟶𝐵) | 
| 9 | 2, 3, 5, 8 | 4syl 19 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ⟶𝐵) | 
| 10 |  | znf1o.w | . . . . . 6
⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) | 
| 11 |  | sseq1 4009 | . . . . . . 7
⊢ (ℤ
= if(𝑁 = 0, ℤ,
(0..^𝑁)) → (ℤ
⊆ ℤ ↔ if(𝑁
= 0, ℤ, (0..^𝑁))
⊆ ℤ)) | 
| 12 |  | sseq1 4009 | . . . . . . 7
⊢
((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔
if(𝑁 = 0, ℤ,
(0..^𝑁)) ⊆
ℤ)) | 
| 13 |  | ssid 4006 | . . . . . . 7
⊢ ℤ
⊆ ℤ | 
| 14 |  | elfzoelz 13699 | . . . . . . . 8
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) | 
| 15 | 14 | ssriv 3987 | . . . . . . 7
⊢
(0..^𝑁) ⊆
ℤ | 
| 16 | 11, 12, 13, 15 | keephyp 4597 | . . . . . 6
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆
ℤ | 
| 17 | 10, 16 | eqsstri 4030 | . . . . 5
⊢ 𝑊 ⊆
ℤ | 
| 18 |  | fssres 6774 | . . . . 5
⊢
(((ℤRHom‘𝑌):ℤ⟶𝐵 ∧ 𝑊 ⊆ ℤ) →
((ℤRHom‘𝑌)
↾ 𝑊):𝑊⟶𝐵) | 
| 19 | 9, 17, 18 | sylancl 586 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) | 
| 20 |  | znf1o.f | . . . . 5
⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) | 
| 21 | 20 | feq1i 6727 | . . . 4
⊢ (𝐹:𝑊⟶𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵) | 
| 22 | 19, 21 | sylibr 234 | . . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊⟶𝐵) | 
| 23 | 20 | fveq1i 6907 | . . . . . . . 8
⊢ (𝐹‘𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) | 
| 24 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) | 
| 25 | 24 | ad2antrl 728 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) | 
| 26 | 23, 25 | eqtrid 2789 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑥) = ((ℤRHom‘𝑌)‘𝑥)) | 
| 27 | 20 | fveq1i 6907 | . . . . . . . 8
⊢ (𝐹‘𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) | 
| 28 |  | fvres 6925 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 29 | 28 | ad2antll 729 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 30 | 27, 29 | eqtrid 2789 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 31 | 26, 30 | eqeq12d 2753 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦))) | 
| 32 |  | simpl 482 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℕ0) | 
| 33 |  | simprl 771 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) | 
| 34 | 17, 33 | sselid 3981 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) | 
| 35 |  | simprr 773 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) | 
| 36 | 17, 35 | sselid 3981 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) | 
| 37 | 1, 4 | zndvds 21568 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ
∧ 𝑦 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) | 
| 38 | 32, 34, 36, 37 | syl3anc 1373 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦))) | 
| 39 |  | elnn0 12528 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) | 
| 40 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℕ) | 
| 41 |  | simprl 771 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊) | 
| 42 | 17, 41 | sselid 3981 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) | 
| 43 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊) | 
| 44 | 17, 43 | sselid 3981 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) | 
| 45 |  | moddvds 16301 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) | 
| 46 | 40, 42, 44, 45 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦))) | 
| 47 | 42 | zred 12722 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℝ) | 
| 48 |  | nnrp 13046 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈
ℝ+) | 
| 50 |  | nnne0 12300 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 51 |  | ifnefalse 4537 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) | 
| 53 | 10, 52 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁)) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑊 = (0..^𝑁)) | 
| 55 | 41, 54 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ (0..^𝑁)) | 
| 56 |  | elfzole1 13707 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥) | 
| 57 | 55, 56 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑥) | 
| 58 |  | elfzolt2 13708 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁) | 
| 59 | 55, 58 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 < 𝑁) | 
| 60 |  | modid 13936 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥) | 
| 61 | 47, 49, 57, 59, 60 | syl22anc 839 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 mod 𝑁) = 𝑥) | 
| 62 | 44 | zred 12722 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℝ) | 
| 63 | 43, 54 | eleqtrd 2843 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ (0..^𝑁)) | 
| 64 |  | elfzole1 13707 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑦) | 
| 66 |  | elfzolt2 13708 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁) | 
| 67 | 63, 66 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 < 𝑁) | 
| 68 |  | modid 13936 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
∧ (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦) | 
| 69 | 62, 49, 65, 67, 68 | syl22anc 839 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑦 mod 𝑁) = 𝑦) | 
| 70 | 61, 69 | eqeq12d 2753 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦)) | 
| 71 | 46, 70 | bitr3d 281 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) | 
| 72 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 = 0) | 
| 73 | 72 | breq1d 5153 | . . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 0 ∥ (𝑥 − 𝑦))) | 
| 74 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑁 = 0 → 𝑁 = 0) | 
| 75 |  | 0nn0 12541 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 76 | 74, 75 | eqeltrdi 2849 | . . . . . . . . . . . 12
⊢ (𝑁 = 0 → 𝑁 ∈
ℕ0) | 
| 77 | 76, 34 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ) | 
| 78 | 76, 36 | sylan 580 | . . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ) | 
| 79 | 77, 78 | zsubcld 12727 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 − 𝑦) ∈ ℤ) | 
| 80 |  | 0dvds 16314 | . . . . . . . . . 10
⊢ ((𝑥 − 𝑦) ∈ ℤ → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0)) | 
| 82 | 77 | zcnd 12723 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℂ) | 
| 83 | 78 | zcnd 12723 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℂ) | 
| 84 | 82, 83 | subeq0ad 11630 | . . . . . . . . 9
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦)) | 
| 85 | 73, 81, 84 | 3bitrd 305 | . . . . . . . 8
⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) | 
| 86 | 71, 85 | jaoian 959 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) | 
| 87 | 39, 86 | sylanb 581 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦)) | 
| 88 | 31, 38, 87 | 3bitrd 305 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦)) | 
| 89 | 88 | biimpd 229 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) | 
| 90 | 89 | ralrimivva 3202 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) | 
| 91 |  | dff13 7275 | . . 3
⊢ (𝐹:𝑊–1-1→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | 
| 92 | 22, 90, 91 | sylanbrc 583 | . 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1→𝐵) | 
| 93 |  | zmodfzo 13934 | . . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) | 
| 94 | 93 | ancoms 458 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁)) | 
| 95 | 53 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁)) | 
| 96 | 94, 95 | eleqtrrd 2844 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊) | 
| 97 |  | zre 12617 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) | 
| 98 |  | modabs2 13945 | . . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) | 
| 99 | 97, 48, 98 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁)) | 
| 100 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ) | 
| 101 | 15, 94 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈
ℤ) | 
| 103 |  | moddvds 16301 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) | 
| 104 | 100, 101,
102, 103 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) | 
| 105 | 99, 104 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)) | 
| 106 |  | nnnn0 12533 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 107 | 106 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈
ℕ0) | 
| 108 | 1, 4 | zndvds 21568 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) | 
| 109 | 107, 101,
102, 108 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))) | 
| 110 | 105, 109 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧)) | 
| 111 | 110 | eqcomd 2743 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) | 
| 112 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) | 
| 113 | 112 | rspceeqv 3645 | . . . . . . . . . 10
⊢ (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 114 | 96, 111, 113 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) →
∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 115 |  | iftrue 4531 | . . . . . . . . . . . . 13
⊢ (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ) | 
| 116 | 115 | eleq2d 2827 | . . . . . . . . . . . 12
⊢ (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ)) | 
| 117 | 116 | biimpar 477 | . . . . . . . . . . 11
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁))) | 
| 118 | 117, 10 | eleqtrrdi 2852 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ 𝑊) | 
| 119 |  | eqidd 2738 | . . . . . . . . . 10
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) →
((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) | 
| 120 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧)) | 
| 121 | 120 | rspceeqv 3645 | . . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 122 | 118, 119,
121 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 123 | 114, 122 | jaoian 959 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 124 | 39, 123 | sylanb 581 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 125 | 27, 28 | eqtrid 2789 | . . . . . . . . 9
⊢ (𝑦 ∈ 𝑊 → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 126 | 125 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))) | 
| 127 | 126 | rexbiia 3092 | . . . . . . 7
⊢
(∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)) | 
| 128 | 124, 127 | sylibr 234 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑧 ∈ ℤ)
→ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) | 
| 129 | 128 | ralrimiva 3146 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ∀𝑧 ∈
ℤ ∃𝑦 ∈
𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)) | 
| 130 | 1, 7, 4 | znzrhfo 21566 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→𝐵) | 
| 131 |  | fofn 6822 | . . . . . 6
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → (ℤRHom‘𝑌) Fn ℤ) | 
| 132 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) | 
| 133 | 132 | rexbidv 3179 | . . . . . . 7
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) | 
| 134 | 133 | ralrn 7108 | . . . . . 6
⊢
((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) | 
| 135 | 130, 131,
134 | 3syl 18 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (∀𝑥 ∈
ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))) | 
| 136 | 129, 135 | mpbird 257 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈ ran
(ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) | 
| 137 |  | forn 6823 | . . . . 5
⊢
((ℤRHom‘𝑌):ℤ–onto→𝐵 → ran (ℤRHom‘𝑌) = 𝐵) | 
| 138 | 130, 137 | syl 17 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ran (ℤRHom‘𝑌) = 𝐵) | 
| 139 | 136, 138 | raleqtrdv 3328 | . . 3
⊢ (𝑁 ∈ ℕ0
→ ∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)) | 
| 140 |  | dffo3 7122 | . . 3
⊢ (𝐹:𝑊–onto→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))) | 
| 141 | 22, 139, 140 | sylanbrc 583 | . 2
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–onto→𝐵) | 
| 142 |  | df-f1o 6568 | . 2
⊢ (𝐹:𝑊–1-1-onto→𝐵 ↔ (𝐹:𝑊–1-1→𝐵 ∧ 𝐹:𝑊–onto→𝐵)) | 
| 143 | 92, 141, 142 | sylanbrc 583 | 1
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑊–1-1-onto→𝐵) |