Metamath Proof Explorer

Theorem znf1o

Description: The function F enumerates all equivalence classes in Z/nZ for each n . When n = 0 , ZZ / 0 ZZ = ZZ / { 0 } ~ZZ so we let W = ZZ ; otherwise W = { 0 , ... , n - 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)

Ref Expression
Hypotheses znf1o.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znf1o.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
znf1o.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
znf1o.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
Assertion znf1o ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 znf1o.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znf1o.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 znf1o.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
4 znf1o.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
5 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
6 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
7 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
8 7 zrhrhm ⊢ ( 𝑌 ∈ Ring → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
9 zringbas ⊢ ℤ = ( Base ‘ ℤring )
10 9 2 rhmf ⊢ ( ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ 𝐵 )
11 5 6 8 10 4syl ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ 𝐵 )
12 sseq1 ⊢ ( ℤ = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) → ( ℤ ⊆ ℤ ↔ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ ) )
13 sseq1 ⊢ ( ( 0 ..^ 𝑁 ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) → ( ( 0 ..^ 𝑁 ) ⊆ ℤ ↔ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ ) )
14 ssid ⊢ ℤ ⊆ ℤ
15 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
16 15 ssriv ⊢ ( 0 ..^ 𝑁 ) ⊆ ℤ
17 12 13 14 16 keephyp ⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ
18 4 17 eqsstri ⊢ 𝑊 ⊆ ℤ
19 fssres ⊢ ( ( ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ 𝐵 ∧ 𝑊 ⊆ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) : 𝑊 ⟶ 𝐵 )
20 11 18 19 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) : 𝑊 ⟶ 𝐵 )
21 3 feq1i ⊢ ( 𝐹 : 𝑊 ⟶ 𝐵 ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) : 𝑊 ⟶ 𝐵 )
22 20 21 sylibr ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 ⟶ 𝐵 )
23 3 fveq1i ⊢ ( 𝐹 ‘ 𝑥 ) = ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑥 )
24 fvres ⊢ ( 𝑥 ∈ 𝑊 → ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
25 24 ad2antrl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
26 23 25 eqtrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
27 3 fveq1i ⊢ ( 𝐹 ‘ 𝑦 ) = ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑦 )
28 fvres ⊢ ( 𝑦 ∈ 𝑊 → ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
29 28 ad2antll ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
30 27 29 eqtrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
31 26 30 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) ) )
32 simpl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑁 ∈ ℕ0 )
33 simprl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ 𝑊 )
34 18 33 sselid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ℤ )
35 simprr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ 𝑊 )
36 18 35 sselid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ℤ )
37 1 7 zndvds ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) ↔ 𝑁 ∥ ( 𝑥 − 𝑦 ) ) )
38 32 34 36 37 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) ↔ 𝑁 ∥ ( 𝑥 − 𝑦 ) ) )
39 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
40 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑁 ∈ ℕ )
41 simprl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ 𝑊 )
42 18 41 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ℤ )
43 simprr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ 𝑊 )
44 18 43 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ℤ )
45 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 mod 𝑁 ) = ( 𝑦 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝑥 − 𝑦 ) ) )
46 40 42 44 45 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝑥 mod 𝑁 ) = ( 𝑦 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝑥 − 𝑦 ) ) )
47 42 zred ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ℝ )
48 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
49 48 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑁 ∈ ℝ+ )
50 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
51 ifnefalse ⊢ ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
52 50 51 syl ⊢ ( 𝑁 ∈ ℕ → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
53 4 52 eqtrid ⊢ ( 𝑁 ∈ ℕ → 𝑊 = ( 0 ..^ 𝑁 ) )
54 53 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑊 = ( 0 ..^ 𝑁 ) )
55 41 54 eleqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ( 0 ..^ 𝑁 ) )
56 elfzole1 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 0 ≤ 𝑥 )
57 55 56 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 0 ≤ 𝑥 )
58 elfzolt2 ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 < 𝑁 )
59 55 58 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 < 𝑁 )
60 modid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < 𝑁 ) ) → ( 𝑥 mod 𝑁 ) = 𝑥 )
61 47 49 57 59 60 syl22anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 mod 𝑁 ) = 𝑥 )
62 44 zred ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ℝ )
63 43 54 eleqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ( 0 ..^ 𝑁 ) )
64 elfzole1 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 0 ≤ 𝑦 )
65 63 64 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 0 ≤ 𝑦 )
66 elfzolt2 ⊢ ( 𝑦 ∈ ( 0 ..^ 𝑁 ) → 𝑦 < 𝑁 )
67 63 66 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 < 𝑁 )
68 modid ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑦 ∧ 𝑦 < 𝑁 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
69 62 49 65 67 68 syl22anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑦 mod 𝑁 ) = 𝑦 )
70 61 69 eqeq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝑥 mod 𝑁 ) = ( 𝑦 mod 𝑁 ) ↔ 𝑥 = 𝑦 ) )
71 46 70 bitr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑁 ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
72 simpl ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑁 = 0 )
73 72 breq1d ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑁 ∥ ( 𝑥 − 𝑦 ) ↔ 0 ∥ ( 𝑥 − 𝑦 ) ) )
74 id ⊢ ( 𝑁 = 0 → 𝑁 = 0 )
75 0nn0 ⊢ 0 ∈ ℕ0
76 74 75 eqeltrdi ⊢ ( 𝑁 = 0 → 𝑁 ∈ ℕ0 )
77 76 34 sylan ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ℤ )
78 76 36 sylan ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ℤ )
79 77 78 zsubcld ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑥 − 𝑦 ) ∈ ℤ )
80 0dvds ⊢ ( ( 𝑥 − 𝑦 ) ∈ ℤ → ( 0 ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 − 𝑦 ) = 0 ) )
81 79 80 syl ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 0 ∥ ( 𝑥 − 𝑦 ) ↔ ( 𝑥 − 𝑦 ) = 0 ) )
82 77 zcnd ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑥 ∈ ℂ )
83 78 zcnd ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → 𝑦 ∈ ℂ )
84 82 83 subeq0ad ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝑥 − 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
85 73 81 84 3bitrd ⊢ ( ( 𝑁 = 0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑁 ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
86 71 85 jaoian ⊢ ( ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑁 ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
87 39 86 sylanb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑁 ∥ ( 𝑥 − 𝑦 ) ↔ 𝑥 = 𝑦 ) )
88 31 38 87 3bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
89 88 biimpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
90 89 ralrimivva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
91 dff13 ⊢ ( 𝐹 : 𝑊 –1-1→ 𝐵 ↔ ( 𝐹 : 𝑊 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑊 ∀ 𝑦 ∈ 𝑊 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
92 22 90 91 sylanbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –1-1→ 𝐵 )
93 zmodfzo ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑧 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
94 93 ancoms ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
95 53 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑊 = ( 0 ..^ 𝑁 ) )
96 94 95 eleqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 mod 𝑁 ) ∈ 𝑊 )
97 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
98 modabs2 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑧 mod 𝑁 ) mod 𝑁 ) = ( 𝑧 mod 𝑁 ) )
99 97 48 98 syl2anr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 mod 𝑁 ) mod 𝑁 ) = ( 𝑧 mod 𝑁 ) )
100 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑁 ∈ ℕ )
101 16 94 sselid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 mod 𝑁 ) ∈ ℤ )
102 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ ℤ )
103 moddvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑧 mod 𝑁 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( 𝑧 mod 𝑁 ) mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝑧 mod 𝑁 ) − 𝑧 ) ) )
104 100 101 102 103 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ( 𝑧 mod 𝑁 ) mod 𝑁 ) = ( 𝑧 mod 𝑁 ) ↔ 𝑁 ∥ ( ( 𝑧 mod 𝑁 ) − 𝑧 ) ) )
105 99 104 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑁 ∥ ( ( 𝑧 mod 𝑁 ) − 𝑧 ) )
106 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
107 106 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
108 1 7 zndvds ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑧 mod 𝑁 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ↔ 𝑁 ∥ ( ( 𝑧 mod 𝑁 ) − 𝑧 ) ) )
109 107 101 102 108 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ↔ 𝑁 ∥ ( ( 𝑧 mod 𝑁 ) − 𝑧 ) ) )
110 105 109 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) )
111 110 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) )
112 fveq2 ⊢ ( 𝑦 = ( 𝑧 mod 𝑁 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) )
113 112 rspceeqv ⊢ ( ( ( 𝑧 mod 𝑁 ) ∈ 𝑊 ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑧 mod 𝑁 ) ) ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
114 96 111 113 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
115 iftrue ⊢ ( 𝑁 = 0 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ℤ )
116 115 eleq2d ⊢ ( 𝑁 = 0 → ( 𝑧 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ↔ 𝑧 ∈ ℤ ) )
117 116 biimpar ⊢ ( ( 𝑁 = 0 ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
118 117 4 eleqtrrdi ⊢ ( ( 𝑁 = 0 ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ 𝑊 )
119 eqidd ⊢ ( ( 𝑁 = 0 ∧ 𝑧 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) )
120 fveq2 ⊢ ( 𝑦 = 𝑧 → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) )
121 120 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑊 ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
122 118 119 121 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑧 ∈ ℤ ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
123 114 122 jaoian ⊢ ( ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ∧ 𝑧 ∈ ℤ ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
124 39 123 sylanb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ℤ ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
125 27 28 eqtrid ⊢ ( 𝑦 ∈ 𝑊 → ( 𝐹 ‘ 𝑦 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
126 125 eqeq2d ⊢ ( 𝑦 ∈ 𝑊 → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) ) )
127 126 rexbiia ⊢ ( ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑦 ) )
128 124 127 sylibr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ℤ ) → ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
129 128 ralrimiva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑧 ∈ ℤ ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
130 1 2 7 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ 𝐵 )
131 fofn ⊢ ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ 𝐵 → ( ℤRHom ‘ 𝑌 ) Fn ℤ )
132 eqeq1 ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) → ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) )
133 132 rexbidv ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) → ( ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) )
134 133 ralrn ⊢ ( ( ℤRHom ‘ 𝑌 ) Fn ℤ → ( ∀ 𝑥 ∈ ran ( ℤRHom ‘ 𝑌 ) ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ ℤ ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) )
135 130 131 134 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑥 ∈ ran ( ℤRHom ‘ 𝑌 ) ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ ℤ ∃ 𝑦 ∈ 𝑊 ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) )
136 129 135 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑥 ∈ ran ( ℤRHom ‘ 𝑌 ) ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) )
137 forn ⊢ ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ 𝐵 → ran ( ℤRHom ‘ 𝑌 ) = 𝐵 )
138 130 137 syl ⊢ ( 𝑁 ∈ ℕ0 → ran ( ℤRHom ‘ 𝑌 ) = 𝐵 )
139 138 raleqdv ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑥 ∈ ran ( ℤRHom ‘ 𝑌 ) ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
140 136 139 mpbid ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) )
141 dffo3 ⊢ ( 𝐹 : 𝑊 –onto→ 𝐵 ↔ ( 𝐹 : 𝑊 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝑊 𝑥 = ( 𝐹 ‘ 𝑦 ) ) )
142 22 140 141 sylanbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –onto→ 𝐵 )
143 df-f1o ⊢ ( 𝐹 : 𝑊 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝑊 –1-1→ 𝐵 ∧ 𝐹 : 𝑊 –onto→ 𝐵 ) )
144 92 142 143 sylanbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –1-1-onto→ 𝐵 )