Theorem znf1o 21040

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.

Step	Hyp	Ref	Expression
1		znf1o.y	. . . . . . 7 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
2	1	zncrng 21033	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
3		crngring 20026	. . . . . 6 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
4		eqid 2731	. . . . . . 7 ⊢ (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
5	4	zrhrhm 20994	. . . . . 6 ⊢ (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
6		zringbas 20957	. . . . . . 7 ⊢ ℤ = (Base‘ℤring)
7		znf1o.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑌)
8	6, 7	rhmf 20213	. . . . . 6 ⊢ ((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) → (ℤRHom‘𝑌):ℤ⟶𝐵)
9	2, 3, 5, 8	4syl 19	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ⟶𝐵)
10		znf1o.w	. . . . . 6 ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
11		sseq1 4003	. . . . . . 7 ⊢ (ℤ = if(𝑁 = 0, ℤ, (0..^𝑁)) → (ℤ ⊆ ℤ ↔ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ))
12		sseq1 4003	. . . . . . 7 ⊢ ((0..^𝑁) = if(𝑁 = 0, ℤ, (0..^𝑁)) → ((0..^𝑁) ⊆ ℤ ↔ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ))
13		ssid 4000	. . . . . . 7 ⊢ ℤ ⊆ ℤ
14		elfzoelz 13614	. . . . . . . 8 ⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ)
15	14	ssriv 3982	. . . . . . 7 ⊢ (0..^𝑁) ⊆ ℤ
16	11, 12, 13, 15	keephyp 4593	. . . . . 6 ⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) ⊆ ℤ
17	10, 16	eqsstri 4012	. . . . 5 ⊢ 𝑊 ⊆ ℤ
18		fssres 6744	. . . . 5 ⊢ (((ℤRHom‘𝑌):ℤ⟶𝐵 ∧ 𝑊 ⊆ ℤ) → ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵)
19	9, 17, 18	sylancl 586	. . . 4 ⊢ (𝑁 ∈ ℕ0 → ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵)
20		znf1o.f	. . . . 5 ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
21	20	feq1i 6695	. . . 4 ⊢ (𝐹:𝑊⟶𝐵 ↔ ((ℤRHom‘𝑌) ↾ 𝑊):𝑊⟶𝐵)
22	19, 21	sylibr 233	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊⟶𝐵)
23	20	fveq1i 6879	. . . . . . . 8 ⊢ (𝐹‘𝑥) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥)
24		fvres 6897	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
25	24	ad2antrl 726	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
26	23, 25	eqtrid 2783	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑥) = ((ℤRHom‘𝑌)‘𝑥))
27	20	fveq1i 6879	. . . . . . . 8 ⊢ (𝐹‘𝑦) = (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦)
28		fvres 6897	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
29	28	ad2antll 727	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌) ↾ 𝑊)‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
30	27, 29	eqtrid 2783	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
31	26, 30	eqeq12d 2747	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦)))
32		simpl 483	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℕ0)
33		simprl 769	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊)
34	17, 33	sselid 3976	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ)
35		simprr 771	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊)
36	17, 35	sselid 3976	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ)
37	1, 4	zndvds 21038	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦)))
38	32, 34, 36, 37	syl3anc 1371	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (((ℤRHom‘𝑌)‘𝑥) = ((ℤRHom‘𝑌)‘𝑦) ↔ 𝑁 ∥ (𝑥 − 𝑦)))
39		elnn0 12456	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℕ ∨ 𝑁 = 0))
40		simpl 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℕ)
41		simprl 769	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ 𝑊)
42	17, 41	sselid 3976	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ)
43		simprr 771	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ 𝑊)
44	17, 43	sselid 3976	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ)
45		moddvds 16190	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦)))
46	40, 42, 44, 45	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑁 ∥ (𝑥 − 𝑦)))
47	42	zred 12648	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℝ)
48		nnrp 12967	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
49	48	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 ∈ ℝ+)
50		nnne0 12228	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
51		ifnefalse 4534	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
52	50, 51	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁))
53	10, 52	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑊 = (0..^𝑁))
54	53	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑊 = (0..^𝑁))
55	41, 54	eleqtrd 2834	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ (0..^𝑁))
56		elfzole1 13622	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0..^𝑁) → 0 ≤ 𝑥)
57	55, 56	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑥)
58		elfzolt2 13623	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 < 𝑁)
59	55, 58	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 < 𝑁)
60		modid 13843	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑁)) → (𝑥 mod 𝑁) = 𝑥)
61	47, 49, 57, 59, 60	syl22anc 837	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 mod 𝑁) = 𝑥)
62	44	zred 12648	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℝ)
63	43, 54	eleqtrd 2834	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ (0..^𝑁))
64		elfzole1 13622	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (0..^𝑁) → 0 ≤ 𝑦)
65	63, 64	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 0 ≤ 𝑦)
66		elfzolt2 13623	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (0..^𝑁) → 𝑦 < 𝑁)
67	63, 66	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 < 𝑁)
68		modid 13843	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (0 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝑦 mod 𝑁) = 𝑦)
69	62, 49, 65, 67, 68	syl22anc 837	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑦 mod 𝑁) = 𝑦)
70	61, 69	eqeq12d 2747	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 mod 𝑁) = (𝑦 mod 𝑁) ↔ 𝑥 = 𝑦))
71	46, 70	bitr3d 280	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦))
72		simpl 483	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑁 = 0)
73	72	breq1d 5151	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 0 ∥ (𝑥 − 𝑦)))
74		id 22	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → 𝑁 = 0)
75		0nn0 12469	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
76	74, 75	eqeltrdi 2840	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → 𝑁 ∈ ℕ0)
77	76, 34	sylan 580	. . . . . . . . . . 11 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℤ)
78	76, 36	sylan 580	. . . . . . . . . . 11 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℤ)
79	77, 78	zsubcld 12653	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑥 − 𝑦) ∈ ℤ)
80		0dvds 16202	. . . . . . . . . 10 ⊢ ((𝑥 − 𝑦) ∈ ℤ → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0))
81	79, 80	syl 17	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (0 ∥ (𝑥 − 𝑦) ↔ (𝑥 − 𝑦) = 0))
82	77	zcnd 12649	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑥 ∈ ℂ)
83	78	zcnd 12649	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → 𝑦 ∈ ℂ)
84	82, 83	subeq0ad 11563	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝑥 − 𝑦) = 0 ↔ 𝑥 = 𝑦))
85	73, 81, 84	3bitrd 304	. . . . . . . 8 ⊢ ((𝑁 = 0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦))
86	71, 85	jaoian 955	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦))
87	39, 86	sylanb 581	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → (𝑁 ∥ (𝑥 − 𝑦) ↔ 𝑥 = 𝑦))
88	31, 38, 87	3bitrd 304	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦))
89	88	biimpd 228	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
90	89	ralrimivva 3199	. . 3 ⊢ (𝑁 ∈ ℕ0 → ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
91		dff13 7238	. . 3 ⊢ (𝐹:𝑊–1-1→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
92	22, 90, 91	sylanbrc 583	. 2 ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1→𝐵)
93		zmodfzo 13841	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
94	93	ancoms 459	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ (0..^𝑁))
95	53	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑊 = (0..^𝑁))
96	94, 95	eleqtrrd 2835	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ 𝑊)
97		zre 12544	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℤ → 𝑧 ∈ ℝ)
98		modabs2 13852	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℝ ∧ 𝑁 ∈ ℝ+) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
99	97, 48, 98	syl2anr 597	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁))
100		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ)
101	15, 94	sselid 3976	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (𝑧 mod 𝑁) ∈ ℤ)
102		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ)
103		moddvds 16190	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
104	100, 101, 102, 103	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑧 mod 𝑁) mod 𝑁) = (𝑧 mod 𝑁) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
105	99, 104	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧))
106		nnnn0 12461	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
107	106	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → 𝑁 ∈ ℕ0)
108	1, 4	zndvds 21038	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑧 mod 𝑁) ∈ ℤ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
109	107, 101, 102, 108	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧) ↔ 𝑁 ∥ ((𝑧 mod 𝑁) − 𝑧)))
110	105, 109	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)) = ((ℤRHom‘𝑌)‘𝑧))
111	110	eqcomd 2737	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
112		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑧 mod 𝑁) → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁)))
113	112	rspceeqv 3629	. . . . . . . . . 10 ⊢ (((𝑧 mod 𝑁) ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘(𝑧 mod 𝑁))) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
114	96, 111, 113	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
115		iftrue 4528	. . . . . . . . . . . . 13 ⊢ (𝑁 = 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = ℤ)
116	115	eleq2d 2818	. . . . . . . . . . . 12 ⊢ (𝑁 = 0 → (𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) ↔ 𝑧 ∈ ℤ))
117	116	biimpar 478	. . . . . . . . . . 11 ⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)))
118	117, 10	eleqtrrdi 2843	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ 𝑊)
119		eqidd 2732	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧))
120		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((ℤRHom‘𝑌)‘𝑦) = ((ℤRHom‘𝑌)‘𝑧))
121	120	rspceeqv 3629	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑊 ∧ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑧)) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
122	118, 119, 121	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑁 = 0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
123	114, 122	jaoian 955	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∨ 𝑁 = 0) ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
124	39, 123	sylanb 581	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
125	27, 28	eqtrid 2783	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑊 → (𝐹‘𝑦) = ((ℤRHom‘𝑌)‘𝑦))
126	125	eqeq2d 2742	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑊 → (((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦)))
127	126	rexbiia 3091	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = ((ℤRHom‘𝑌)‘𝑦))
128	124, 127	sylibr 233	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑧 ∈ ℤ) → ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))
129	128	ralrimiva 3145	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦))
130	1, 7, 4	znzrhfo 21036	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ–onto→𝐵)
131		fofn 6794	. . . . . 6 ⊢ ((ℤRHom‘𝑌):ℤ–onto→𝐵 → (ℤRHom‘𝑌) Fn ℤ)
132		eqeq1 2735	. . . . . . . 8 ⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (𝑥 = (𝐹‘𝑦) ↔ ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)))
133	132	rexbidv 3177	. . . . . . 7 ⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑧) → (∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)))
134	133	ralrn 7074	. . . . . 6 ⊢ ((ℤRHom‘𝑌) Fn ℤ → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)))
135	130, 131, 134	3syl 18	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑧 ∈ ℤ ∃𝑦 ∈ 𝑊 ((ℤRHom‘𝑌)‘𝑧) = (𝐹‘𝑦)))
136	129, 135	mpbird 256	. . . 4 ⊢ (𝑁 ∈ ℕ0 → ∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))
137		forn 6795	. . . . . 6 ⊢ ((ℤRHom‘𝑌):ℤ–onto→𝐵 → ran (ℤRHom‘𝑌) = 𝐵)
138	130, 137	syl 17	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → ran (ℤRHom‘𝑌) = 𝐵)
139	138	raleqdv 3324	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (∀𝑥 ∈ ran (ℤRHom‘𝑌)∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦) ↔ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)))
140	136, 139	mpbid 231	. . 3 ⊢ (𝑁 ∈ ℕ0 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦))
141		dffo3 7088	. . 3 ⊢ (𝐹:𝑊–onto→𝐵 ↔ (𝐹:𝑊⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝑊 𝑥 = (𝐹‘𝑦)))
142	22, 140, 141	sylanbrc 583	. 2 ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–onto→𝐵)
143		df-f1o 6539	. 2 ⊢ (𝐹:𝑊–1-1-onto→𝐵 ↔ (𝐹:𝑊–1-1→𝐵 ∧ 𝐹:𝑊–onto→𝐵))
144	92, 142, 143	sylanbrc 583	1 ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ⊆ wss 3944  ifcif 4522   class class class wbr 5141  ran crn 5670   ↾ cres 5671   Fn wfn 6527  ⟶wf 6528  –1-1→wf1 6529  –onto→wfo 6530  –1-1-onto→wf1o 6531  ‘cfv 6532  (class class class)co 7393  ℝcr 11091  0cc0 11092   < clt 11230   ≤ cle 11231   − cmin 11426  ℕcn 12194  ℕ₀cn0 12454  ℤcz 12540  ℝ⁺crp 12956  ..^cfzo 13609   mod cmo 13816   ∥ cdvds 16179  Basecbs 17126  Ringcrg 20014  CRingccrg 20015   RingHom crh 20198  ℤ_ringczring 20951  ℤRHomczrh 20982  ℤ/nℤczn 20985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170  ax-addf 11171  ax-mulf 11172

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-tpos 8193  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-er 8686  df-ec 8688  df-qs 8692  df-map 8805  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-sup 9419  df-inf 9420  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-z 12541  df-dec 12660  df-uz 12805  df-rp 12957  df-fz 13467  df-fzo 13610  df-fl 13739  df-mod 13817  df-seq 13949  df-dvds 16180  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-0g 17369  df-imas 17436  df-qus 17437  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-mhm 18647  df-grp 18797  df-minusg 18798  df-sbg 18799  df-mulg 18923  df-subg 18975  df-nsg 18976  df-eqg 18977  df-ghm 19056  df-cmn 19614  df-abl 19615  df-mgp 19947  df-ur 19964  df-ring 20016  df-cring 20017  df-oppr 20102  df-dvdsr 20123  df-rnghom 20201  df-subrg 20310  df-lmod 20422  df-lss 20492  df-lsp 20532  df-sra 20734  df-rgmod 20735  df-lidl 20736  df-rsp 20737  df-2idl 20803  df-cnfld 20879  df-zring 20952  df-zrh 20986  df-zn 20989

This theorem is referenced by:  zzngim  21041  znleval  21043  zntoslem  21045  znhash  21047  znunithash  21053  dchrisumlem1  26919