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 
|- Y = ( Z/nZ ` N )
znf1o.b 
|- B = ( Base ` Y )
znf1o.f 
|- F = ( ( ZRHom ` Y ) |` W )
znf1o.w 
|- W = if ( N = 0 , ZZ , ( 0 ..^ N ) )
Assertion znf1o 
|- ( N e. NN0 -> F : W -1-1-onto-> B )

Proof

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