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	$⊢ Y = ℤ / N ℤ$
	znf1o.b	$⊢ B = {Base}_{Y}$
	znf1o.f	$⊢ F = {ℤRHom (Y) ↾}_{W}$
	znf1o.w	$⊢ W = if (N = 0, ℤ, (0 ..^N))$
Assertion	znf1o	$⊢ N \in ℕ_{0} \to F : W \underset{1-1 onto}{⟶} B$

Proof

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

Metamath Proof Explorer

Theorem znf1o

Proof