ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  znf1o GIF version

Theorem znf1o 14207
Description: The function 𝐹 enumerates all equivalence classes in ℤ/n for each 𝑛. When 𝑛 = 0, ℤ / 0ℤ = ℤ / {0} ≈ ℤ so we let 𝑊 = ℤ; otherwise 𝑊 = {0, ..., 𝑛 − 1} enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
Hypotheses
Ref Expression
znf1o.y 𝑌 = (ℤ/nℤ‘𝑁)
znf1o.b 𝐵 = (Base‘𝑌)
znf1o.f 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
znf1o.w 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
Assertion
Ref Expression
znf1o (𝑁 ∈ ℕ0𝐹:𝑊1-1-onto𝐵)

Proof of Theorem znf1o
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 znf1o.y . . . . . . 7 𝑌 = (ℤ/nℤ‘𝑁)
21zncrng 14201 . . . . . 6 (𝑁 ∈ ℕ0𝑌 ∈ CRing)
3 crngring 13564 . . . . . 6 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
4 eqid 2196 . . . . . . 7 (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
54zrhrhm 14179 . . . . . 6 (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
6 zringbas 14152 . . . . . . 7 ℤ = (Base‘ℤring)
7 znf1o.b . . . . . . 7 𝐵 = (Base‘𝑌)
86, 7rhmf 13719 . . . . . 6 ((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) → (ℤRHom‘𝑌):ℤ⟶𝐵)
92, 3, 5, 84syl 18 . . . . 5 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ⟶𝐵)
10 znf1o.w . . . . . . . 8 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
11 simpr 110 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑁 = 0) → 𝑁 = 0)
1211iftrued 3568 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑁 = 0) → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ)
1310, 12eqtrid 2241 . . . . . . 7 ((𝑁 ∈ ℕ0𝑁 = 0) → 𝑊 = ℤ)
14 ssid 3203 . . . . . . 7 ℤ ⊆ ℤ
1513, 14eqsstrdi 3235 . . . . . 6 ((𝑁 ∈ ℕ0𝑁 = 0) → 𝑊 ⊆ ℤ)
16 simpr 110 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ ¬ 𝑁 = 0) → ¬ 𝑁 = 0)
1716iffalsed 3571 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ ¬ 𝑁 = 0) → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
1810, 17eqtrid 2241 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ ¬ 𝑁 = 0) → 𝑊 = (0..^𝑁))
19 elfzoelz 10222 . . . . . . . 8 (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ)
2019ssriv 3187 . . . . . . 7 (0..^𝑁) ⊆ ℤ
2118, 20eqsstrdi 3235 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ ¬ 𝑁 = 0) → 𝑊 ⊆ ℤ)
22 nn0z 9346 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
23 0z 9337 . . . . . . . 8 0 ∈ ℤ
24 zdceq 9401 . . . . . . . 8 ((𝑁 ∈ ℤ ∧ 0 ∈ ℤ) → DECID 𝑁 = 0)
2522, 23, 24sylancl 413 . . . . . . 7 (𝑁 ∈ ℕ0DECID 𝑁 = 0)
26 exmiddc 837 . . . . . . 7 (DECID 𝑁 = 0 → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
2725, 26syl 14 . . . . . 6 (𝑁 ∈ ℕ0 → (𝑁 = 0 ∨ ¬ 𝑁 = 0))
2815, 21, 27mpjaodan 799 . . . . 5 (𝑁 ∈ ℕ0𝑊 ⊆ ℤ)
299, 28fssresd 5434 . . . 4 (𝑁 ∈ ℕ0 → ((ℤRHom‘𝑌) ↾ 𝑊):𝑊𝐵)
30 znf1o.f . . . . 5 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
3130feq1i 5400 . . . 4 (𝐹:𝑊𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊𝐵)
3229, 31sylibr 134 . . 3 (𝑁 ∈ ℕ0𝐹:𝑊𝐵)
3330fveq1i 5559 . . . . . . . 8 (𝐹𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥)
34 fvres 5582 . . . . . . . . 9 (𝑥𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
3534ad2antrl 490 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
3633, 35eqtrid 2241 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝐹𝑥) = ((ℤRHom‘𝑌)‘𝑥))
3730fveq1i 5559 . . . . . . . 8 (𝐹𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦)
38 fvres 5582 . . . . . . . . 9 (𝑦𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
3938ad2antll 491 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
4037, 39eqtrid 2241 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝐹𝑦) = ((ℤRHom‘𝑌)‘𝑦))
4136, 40eqeq12d 2211 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦)))
42 simpl 109 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℕ0)
4328adantr 276 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑊 ⊆ ℤ)
44 simprl 529 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥𝑊)
4543, 44sseldd 3184 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
46 simprr 531 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦𝑊)
4743, 46sseldd 3184 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
481, 4zndvds 14205 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥𝑦)))
4942, 45, 47, 48syl3anc 1249 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥𝑦)))
50 elnn0 9251 . . . . . . 7 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
51 simpl 109 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℕ)
5251nnnn0d 9302 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℕ0)
5352, 28syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑊 ⊆ ℤ)
54 simprl 529 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥𝑊)
5553, 54sseldd 3184 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
56 simprr 531 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦𝑊)
5753, 56sseldd 3184 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
58 moddvds 11964 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥𝑦)))
5951, 55, 57, 58syl3anc 1249 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥𝑦)))
60 zq 9700 . . . . . . . . . . . 12 (𝑥 ∈ ℤ → 𝑥 ∈ ℚ)
6155, 60syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℚ)
62 nnq 9707 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℚ)
6362adantr 276 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℚ)
64 nnne0 9018 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
65 ifnefalse 3572 . . . . . . . . . . . . . . . 16 (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
6664, 65syl 14 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
6710, 66eqtrid 2241 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁))
6867adantr 276 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑊 = (0..^𝑁))
6954, 68eleqtrd 2275 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ (0..^𝑁))
70 elfzole1 10231 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥)
7169, 70syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 0 ≤ 𝑥)
72 elfzolt2 10232 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁)
7369, 72syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 < 𝑁)
74 modqid 10441 . . . . . . . . . . 11 (((𝑥 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (0 ≤ 𝑥𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥)
7561, 63, 71, 73, 74syl22anc 1250 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑥 mod 𝑁) = 𝑥)
76 zq 9700 . . . . . . . . . . . 12 (𝑦 ∈ ℤ → 𝑦 ∈ ℚ)
7757, 76syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℚ)
7856, 68eleqtrd 2275 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ (0..^𝑁))
79 elfzole1 10231 . . . . . . . . . . . 12 (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦)
8078, 79syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 0 ≤ 𝑦)
81 elfzolt2 10232 . . . . . . . . . . . 12 (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁)
8278, 81syl 14 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 < 𝑁)
83 modqid 10441 . . . . . . . . . . 11 (((𝑦 ∈ ℚ ∧ 𝑁 ∈ ℚ) ∧ (0 ≤ 𝑦𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦)
8477, 63, 80, 82, 83syl22anc 1250 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑦 mod 𝑁) = 𝑦)
8575, 84eqeq12d 2211 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦))
8659, 85bitr3d 190 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
87 simpl 109 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 = 0)
8887breq1d 4043 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 0 ∥ (𝑥𝑦)))
89 id 19 . . . . . . . . . . . . 13 (𝑁 = 0 → 𝑁 = 0)
90 0nn0 9264 . . . . . . . . . . . . 13 0 ∈ ℕ0
9189, 90eqeltrdi 2287 . . . . . . . . . . . 12 (𝑁 = 0 → 𝑁 ∈ ℕ0)
9291, 45sylan 283 . . . . . . . . . . 11 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
9391, 47sylan 283 . . . . . . . . . . 11 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
9492, 93zsubcld 9453 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑥𝑦) ∈ ℤ)
95 0dvds 11976 . . . . . . . . . 10 ((𝑥𝑦) ∈ ℤ → (0 ∥ (𝑥𝑦) ↔ (𝑥𝑦) = 0))
9694, 95syl 14 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (0 ∥ (𝑥𝑦) ↔ (𝑥𝑦) = 0))
9792zcnd 9449 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℂ)
9893zcnd 9449 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℂ)
9997, 98subeq0ad 8347 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥𝑦) = 0 ↔ 𝑥 = 𝑦))
10088, 96, 993bitrd 214 . . . . . . . 8 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
10186, 100jaoian 796 . . . . . . 7 (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
10250, 101sylanb 284 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
10341, 49, 1023bitrd 214 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
104103biimpd 144 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
105104ralrimivva 2579 . . 3 (𝑁 ∈ ℕ0 → ∀𝑥𝑊𝑦𝑊 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
106 dff13 5815 . . 3 (𝐹:𝑊1-1𝐵 ↔ (𝐹:𝑊𝐵 ∧ ∀𝑥𝑊𝑦𝑊 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
10732, 105, 106sylanbrc 417 . 2 (𝑁 ∈ ℕ0𝐹:𝑊1-1𝐵)
108 zmodfzo 10439 . . . . . . . . . . . 12 ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
109108ancoms 268 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
11067adantr 276 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁))
111109, 110eleqtrrd 2276 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊)
112 zq 9700 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℤ → 𝑧 ∈ ℚ)
113112adantl 277 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℚ)
11462adantr 276 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℚ)
115 nngt0 9015 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → 0 < 𝑁)
116115adantr 276 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 0 < 𝑁)
117 modqabs2 10450 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℚ ∧ 𝑁 ∈ ℚ ∧ 0 < 𝑁) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
118113, 114, 116, 117syl3anc 1249 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
119 simpl 109 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ)
12020, 109sselid 3181 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ)
121 simpr 110 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
122 moddvds 11964 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
123119, 120, 121, 122syl3anc 1249 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
124118, 123mpbid 147 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))
125 nnnn0 9256 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
126125adantr 276 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ0)
1271, 4zndvds 14205 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
128126, 120, 121, 127syl3anc 1249 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
129124, 128mpbird 167 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧))
130129eqcomd 2202 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
131 fveq2 5558 . . . . . . . . . . 11 (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
132131rspceeqv 2886 . . . . . . . . . 10 (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
133111, 130, 132syl2anc 411 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
134 iftrue 3566 . . . . . . . . . . . . 13 (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ)
135134eleq2d 2266 . . . . . . . . . . . 12 (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ))
136135biimpar 297 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)))
137136, 10eleqtrrdi 2290 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧𝑊)
138 eqidd 2197 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧))
139 fveq2 5558 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧))
140139rspceeqv 2886 . . . . . . . . . 10 ((𝑧𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
141137, 138, 140syl2anc 411 . . . . . . . . 9 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
142133, 141jaoian 796 . . . . . . . 8 (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
14350, 142sylanb 284 . . . . . . 7 ((𝑁 ∈ ℕ0𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
14437, 38eqtrid 2241 . . . . . . . . 9 (𝑦𝑊 → (𝐹𝑦) = ((ℤRHom‘𝑌)‘𝑦))
145144eqeq2d 2208 . . . . . . . 8 (𝑦𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)))
146145rexbiia 2512 . . . . . . 7 (∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦) ↔ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
147143, 146sylibr 134 . . . . . 6 ((𝑁 ∈ ℕ0𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦))
148147ralrimiva 2570 . . . . 5 (𝑁 ∈ ℕ0 → ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦))
1491, 7, 4znzrhfo 14204 . . . . . 6 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ–onto𝐵)
150 fofn 5482 . . . . . 6 ((ℤRHom‘𝑌):ℤ–onto𝐵 → (ℤRHom‘𝑌) Fn ℤ)
151 eqeq1 2203 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
152151rexbidv 2498 . . . . . . 7 (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
153152ralrn 5700 . . . . . 6 ((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
154149, 150, 1533syl 17 . . . . 5 (𝑁 ∈ ℕ0 → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
155148, 154mpbird 167 . . . 4 (𝑁 ∈ ℕ0 → ∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦))
156 forn 5483 . . . . 5 ((ℤRHom‘𝑌):ℤ–onto𝐵 → ran (ℤRHom‘𝑌) = 𝐵)
157149, 156syl 14 . . . 4 (𝑁 ∈ ℕ0 → ran (ℤRHom‘𝑌) = 𝐵)
158155, 157raleqtrdv 2701 . . 3 (𝑁 ∈ ℕ0 → ∀𝑥𝐵𝑦𝑊 𝑥 = (𝐹𝑦))
159 dffo3 5709 . . 3 (𝐹:𝑊onto𝐵 ↔ (𝐹:𝑊𝐵 ∧ ∀𝑥𝐵𝑦𝑊 𝑥 = (𝐹𝑦)))
16032, 158, 159sylanbrc 417 . 2 (𝑁 ∈ ℕ0𝐹:𝑊onto𝐵)
161 df-f1o 5265 . 2 (𝐹:𝑊1-1-onto𝐵 ↔ (𝐹:𝑊1-1𝐵𝐹:𝑊onto𝐵))
162107, 160, 161sylanbrc 417 1 (𝑁 ∈ ℕ0𝐹:𝑊1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835   = wceq 1364  wcel 2167  wne 2367  wral 2475  wrex 2476  wss 3157  ifcif 3561   class class class wbr 4033  ran crn 4664  cres 4665   Fn wfn 5253  wf 5254  1-1wf1 5255  ontowfo 5256  1-1-ontowf1o 5257  cfv 5258  (class class class)co 5922  0cc0 7879   < clt 8061  cle 8062  cmin 8197  cn 8990  0cn0 9249  cz 9326  cq 9693  ..^cfzo 10217   mod cmo 10414  cdvds 11952  Basecbs 12678  Ringcrg 13552  CRingccrg 13553   RingHom crh 13706  ringczring 14146  ℤRHomczrh 14167  ℤ/nczn 14169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996  ax-pre-mulext 7997  ax-arch 7998  ax-addf 8001  ax-mulf 8002
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-tp 3630  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-tpos 6303  df-recs 6363  df-frec 6449  df-er 6592  df-ec 6594  df-qs 6598  df-map 6709  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-div 8700  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-5 9052  df-6 9053  df-7 9054  df-8 9055  df-9 9056  df-n0 9250  df-z 9327  df-dec 9458  df-uz 9602  df-q 9694  df-rp 9729  df-fz 10084  df-fzo 10218  df-fl 10360  df-mod 10415  df-seqfrec 10540  df-cj 11007  df-abs 11164  df-dvds 11953  df-struct 12680  df-ndx 12681  df-slot 12682  df-base 12684  df-sets 12685  df-iress 12686  df-plusg 12768  df-mulr 12769  df-starv 12770  df-sca 12771  df-vsca 12772  df-ip 12773  df-tset 12774  df-ple 12775  df-ds 12777  df-unif 12778  df-0g 12929  df-topgen 12931  df-iimas 12945  df-qus 12946  df-mgm 12999  df-sgrp 13045  df-mnd 13058  df-mhm 13091  df-grp 13135  df-minusg 13136  df-sbg 13137  df-mulg 13250  df-subg 13300  df-nsg 13301  df-eqg 13302  df-ghm 13371  df-cmn 13416  df-abl 13417  df-mgp 13477  df-rng 13489  df-ur 13516  df-srg 13520  df-ring 13554  df-cring 13555  df-oppr 13624  df-dvdsr 13645  df-rhm 13708  df-subrg 13775  df-lmod 13845  df-lssm 13909  df-lsp 13943  df-sra 13991  df-rgmod 13992  df-lidl 14025  df-rsp 14026  df-2idl 14056  df-bl 14102  df-mopn 14103  df-fg 14105  df-metu 14106  df-cnfld 14113  df-zring 14147  df-zrh 14170  df-zn 14172
This theorem is referenced by:  znleval  14209  znfi  14211  znhash  14212
  Copyright terms: Public domain W3C validator