MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  znf1o Structured version   Visualization version   GIF version

Theorem znf1o 19819
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 19812 . . . . . 6 (𝑁 ∈ ℕ0𝑌 ∈ CRing)
3 crngring 18479 . . . . . 6 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
4 eqid 2621 . . . . . . 7 (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
54zrhrhm 19779 . . . . . 6 (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
6 zringbas 19743 . . . . . . 7 ℤ = (Base‘ℤring)
7 znf1o.b . . . . . . 7 𝐵 = (Base‘𝑌)
86, 7rhmf 18647 . . . . . 6 ((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) → (ℤRHom‘𝑌):ℤ⟶𝐵)
92, 3, 5, 84syl 19 . . . . 5 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ⟶𝐵)
10 znf1o.w . . . . . 6 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
11 sseq1 3605 . . . . . . 7 (ℤ = if(𝑁 = 0, ℤ, (0..^𝑁)) → (ℤ ⊆ ℤ ↔ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ))
12 sseq1 3605 . . . . . . 7 ((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ))
13 ssid 3603 . . . . . . 7 ℤ ⊆ ℤ
14 elfzoelz 12411 . . . . . . . 8 (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ)
1514ssriv 3587 . . . . . . 7 (0..^𝑁) ⊆ ℤ
1611, 12, 13, 15keephyp 4124 . . . . . 6 if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ
1710, 16eqsstri 3614 . . . . 5 𝑊 ⊆ ℤ
18 fssres 6027 . . . . 5 (((ℤRHom‘𝑌):ℤ⟶𝐵𝑊 ⊆ ℤ) → ((ℤRHom‘𝑌) ↾ 𝑊):𝑊𝐵)
199, 17, 18sylancl 693 . . . 4 (𝑁 ∈ ℕ0 → ((ℤRHom‘𝑌) ↾ 𝑊):𝑊𝐵)
20 znf1o.f . . . . 5 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
2120feq1i 5993 . . . 4 (𝐹:𝑊𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊𝐵)
2219, 21sylibr 224 . . 3 (𝑁 ∈ ℕ0𝐹:𝑊𝐵)
2320fveq1i 6149 . . . . . . . 8 (𝐹𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥)
24 fvres 6164 . . . . . . . . 9 (𝑥𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
2524ad2antrl 763 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
2623, 25syl5eq 2667 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝐹𝑥) = ((ℤRHom‘𝑌)‘𝑥))
2720fveq1i 6149 . . . . . . . 8 (𝐹𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦)
28 fvres 6164 . . . . . . . . 9 (𝑦𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
2928ad2antll 764 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
3027, 29syl5eq 2667 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝐹𝑦) = ((ℤRHom‘𝑌)‘𝑦))
3126, 30eqeq12d 2636 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦)))
32 simpl 473 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℕ0)
33 simprl 793 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥𝑊)
3417, 33sseldi 3581 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
35 simprr 795 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦𝑊)
3617, 35sseldi 3581 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
371, 4zndvds 19817 . . . . . . 7 ((𝑁 ∈ ℕ0𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥𝑦)))
3832, 34, 36, 37syl3anc 1323 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥𝑦)))
39 elnn0 11238 . . . . . . 7 (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
40 simpl 473 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℕ)
41 simprl 793 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥𝑊)
4217, 41sseldi 3581 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
43 simprr 795 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦𝑊)
4417, 43sseldi 3581 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
45 moddvds 14915 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥𝑦)))
4640, 42, 44, 45syl3anc 1323 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥𝑦)))
4742zred 11426 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℝ)
48 nnrp 11786 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
4948adantr 481 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 ∈ ℝ+)
50 nnne0 10997 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
51 ifnefalse 4070 . . . . . . . . . . . . . . . 16 (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
5250, 51syl 17 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
5310, 52syl5eq 2667 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁))
5453adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑊 = (0..^𝑁))
5541, 54eleqtrd 2700 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ (0..^𝑁))
56 elfzole1 12419 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥)
5755, 56syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 0 ≤ 𝑥)
58 elfzolt2 12420 . . . . . . . . . . . 12 (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁)
5955, 58syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 < 𝑁)
60 modid 12635 . . . . . . . . . . 11 (((𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤ 𝑥𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥)
6147, 49, 57, 59, 60syl22anc 1324 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑥 mod 𝑁) = 𝑥)
6244zred 11426 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℝ)
6343, 54eleqtrd 2700 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ (0..^𝑁))
64 elfzole1 12419 . . . . . . . . . . . 12 (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦)
6563, 64syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 0 ≤ 𝑦)
66 elfzolt2 12420 . . . . . . . . . . . 12 (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁)
6763, 66syl 17 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 < 𝑁)
68 modid 12635 . . . . . . . . . . 11 (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤ 𝑦𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦)
6962, 49, 65, 67, 68syl22anc 1324 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑦 mod 𝑁) = 𝑦)
7061, 69eqeq12d 2636 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦))
7146, 70bitr3d 270 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
72 simpl 473 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑁 = 0)
7372breq1d 4623 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 0 ∥ (𝑥𝑦)))
74 id 22 . . . . . . . . . . . . 13 (𝑁 = 0 → 𝑁 = 0)
75 0nn0 11251 . . . . . . . . . . . . 13 0 ∈ ℕ0
7674, 75syl6eqel 2706 . . . . . . . . . . . 12 (𝑁 = 0 → 𝑁 ∈ ℕ0)
7776, 34sylan 488 . . . . . . . . . . 11 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℤ)
7876, 36sylan 488 . . . . . . . . . . 11 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℤ)
7977, 78zsubcld 11431 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑥𝑦) ∈ ℤ)
80 0dvds 14926 . . . . . . . . . 10 ((𝑥𝑦) ∈ ℤ → (0 ∥ (𝑥𝑦) ↔ (𝑥𝑦) = 0))
8179, 80syl 17 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (0 ∥ (𝑥𝑦) ↔ (𝑥𝑦) = 0))
8277zcnd 11427 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑥 ∈ ℂ)
8378zcnd 11427 . . . . . . . . . 10 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → 𝑦 ∈ ℂ)
8482, 83subeq0ad 10346 . . . . . . . . 9 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝑥𝑦) = 0 ↔ 𝑥 = 𝑦))
8573, 81, 843bitrd 294 . . . . . . . 8 ((𝑁 = 0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
8671, 85jaoian 823 . . . . . . 7 (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
8739, 86sylanb 489 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → (𝑁 ∥ (𝑥𝑦) ↔ 𝑥 = 𝑦))
8831, 38, 873bitrd 294 . . . . 5 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) ↔ 𝑥 = 𝑦))
8988biimpd 219 . . . 4 ((𝑁 ∈ ℕ0 ∧ (𝑥𝑊𝑦𝑊)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
9089ralrimivva 2965 . . 3 (𝑁 ∈ ℕ0 → ∀𝑥𝑊𝑦𝑊 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
91 dff13 6466 . . 3 (𝐹:𝑊1-1𝐵 ↔ (𝐹:𝑊𝐵 ∧ ∀𝑥𝑊𝑦𝑊 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
9222, 90, 91sylanbrc 697 . 2 (𝑁 ∈ ℕ0𝐹:𝑊1-1𝐵)
93 zmodfzo 12633 . . . . . . . . . . . 12 ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
9493ancoms 469 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
9553adantr 481 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁))
9694, 95eleqtrrd 2701 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊)
97 zre 11325 . . . . . . . . . . . . . 14 (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
98 modabs2 12644 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
9997, 48, 98syl2anr 495 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
100 simpl 473 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ)
10115, 94sseldi 3581 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ)
102 simpr 477 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
103 moddvds 14915 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
104100, 101, 102, 103syl3anc 1323 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
10599, 104mpbid 222 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))
106 nnnn0 11243 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
107106adantr 481 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ0)
1081, 4zndvds 19817 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
109107, 101, 102, 108syl3anc 1323 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
110105, 109mpbird 247 . . . . . . . . . . 11 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧))
111110eqcomd 2627 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
112 fveq2 6148 . . . . . . . . . . . 12 (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
113112eqeq2d 2631 . . . . . . . . . . 11 (𝑦 = (𝑧 mod 𝑁) → (((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))))
114113rspcev 3295 . . . . . . . . . 10 (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
11596, 111, 114syl2anc 692 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
116 iftrue 4064 . . . . . . . . . . . . 13 (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ)
117116eleq2d 2684 . . . . . . . . . . . 12 (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ))
118117biimpar 502 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)))
119118, 10syl6eleqr 2709 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧𝑊)
120 eqidd 2622 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧))
121 fveq2 6148 . . . . . . . . . . . 12 (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧))
122121eqeq2d 2631 . . . . . . . . . . 11 (𝑦 = 𝑧 → (((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)))
123122rspcev 3295 . . . . . . . . . 10 ((𝑧𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
124119, 120, 123syl2anc 692 . . . . . . . . 9 ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
125115, 124jaoian 823 . . . . . . . 8 (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
12639, 125sylanb 489 . . . . . . 7 ((𝑁 ∈ ℕ0𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
12727, 28syl5eq 2667 . . . . . . . . 9 (𝑦𝑊 → (𝐹𝑦) = ((ℤRHom‘𝑌)‘𝑦))
128127eqeq2d 2631 . . . . . . . 8 (𝑦𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)))
129128rexbiia 3033 . . . . . . 7 (∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦) ↔ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
130126, 129sylibr 224 . . . . . 6 ((𝑁 ∈ ℕ0𝑧 ∈ ℤ) → ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦))
131130ralrimiva 2960 . . . . 5 (𝑁 ∈ ℕ0 → ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦))
1321, 7, 4znzrhfo 19815 . . . . . 6 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ–onto𝐵)
133 fofn 6074 . . . . . 6 ((ℤRHom‘𝑌):ℤ–onto𝐵 → (ℤRHom‘𝑌) Fn ℤ)
134 eqeq1 2625 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
135134rexbidv 3045 . . . . . . 7 (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
136135ralrn 6318 . . . . . 6 ((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
137132, 133, 1363syl 18 . . . . 5 (𝑁 ∈ ℕ0 → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹𝑦)))
138131, 137mpbird 247 . . . 4 (𝑁 ∈ ℕ0 → ∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦))
139 forn 6075 . . . . . 6 ((ℤRHom‘𝑌):ℤ–onto𝐵 → ran (ℤRHom‘𝑌) = 𝐵)
140132, 139syl 17 . . . . 5 (𝑁 ∈ ℕ0 → ran (ℤRHom‘𝑌) = 𝐵)
141140raleqdv 3133 . . . 4 (𝑁 ∈ ℕ0 → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦𝑊 𝑥 = (𝐹𝑦) ↔ ∀𝑥𝐵𝑦𝑊 𝑥 = (𝐹𝑦)))
142138, 141mpbid 222 . . 3 (𝑁 ∈ ℕ0 → ∀𝑥𝐵𝑦𝑊 𝑥 = (𝐹𝑦))
143 dffo3 6330 . . 3 (𝐹:𝑊onto𝐵 ↔ (𝐹:𝑊𝐵 ∧ ∀𝑥𝐵𝑦𝑊 𝑥 = (𝐹𝑦)))
14422, 142, 143sylanbrc 697 . 2 (𝑁 ∈ ℕ0𝐹:𝑊onto𝐵)
145 df-f1o 5854 . 2 (𝐹:𝑊1-1-onto𝐵 ↔ (𝐹:𝑊1-1𝐵𝐹:𝑊onto𝐵))
14692, 144, 145sylanbrc 697 1 (𝑁 ∈ ℕ0𝐹:𝑊1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  wss 3555  ifcif 4058   class class class wbr 4613  ran crn 5075  cres 5076   Fn wfn 5842  wf 5843  1-1wf1 5844  ontowfo 5845  1-1-ontowf1o 5846  cfv 5847  (class class class)co 6604  cr 9879  0cc0 9880   < clt 10018  cle 10019  cmin 10210  cn 10964  0cn0 11236  cz 11321  +crp 11776  ..^cfzo 12406   mod cmo 12608  cdvds 14907  Basecbs 15781  Ringcrg 18468  CRingccrg 18469   RingHom crh 18633  ringzring 19737  ℤRHomczrh 19767  ℤ/nczn 19770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958  ax-addf 9959  ax-mulf 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-tpos 7297  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-ec 7689  df-qs 7693  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-sup 8292  df-inf 8293  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-rp 11777  df-fz 12269  df-fzo 12407  df-fl 12533  df-mod 12609  df-seq 12742  df-dvds 14908  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-starv 15877  df-sca 15878  df-vsca 15879  df-ip 15880  df-tset 15881  df-ple 15882  df-ds 15885  df-unif 15886  df-0g 16023  df-imas 16089  df-qus 16090  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-mhm 17256  df-grp 17346  df-minusg 17347  df-sbg 17348  df-mulg 17462  df-subg 17512  df-nsg 17513  df-eqg 17514  df-ghm 17579  df-cmn 18116  df-abl 18117  df-mgp 18411  df-ur 18423  df-ring 18470  df-cring 18471  df-oppr 18544  df-dvdsr 18562  df-rnghom 18636  df-subrg 18699  df-lmod 18786  df-lss 18852  df-lsp 18891  df-sra 19091  df-rgmod 19092  df-lidl 19093  df-rsp 19094  df-2idl 19151  df-cnfld 19666  df-zring 19738  df-zrh 19771  df-zn 19774
This theorem is referenced by:  zzngim  19820  znleval  19822  zntoslem  19824  znhash  19826  znunithash  19832  dchrisumlem1  25078
  Copyright terms: Public domain W3C validator