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=/N
znf1o.b B=BaseY
znf1o.f F=ℤRHomYW
znf1o.w W=ifN=00..^N
Assertion znf1o N0F:W1-1 ontoB

Proof

Step Hyp Ref Expression
1 znf1o.y Y=/N
2 znf1o.b B=BaseY
3 znf1o.f F=ℤRHomYW
4 znf1o.w W=ifN=00..^N
5 1 zncrng N0YCRing
6 crngring YCRingYRing
7 eqid ℤRHomY=ℤRHomY
8 7 zrhrhm YRingℤRHomYringRingHomY
9 zringbas =Basering
10 9 2 rhmf ℤRHomYringRingHomYℤRHomY:B
11 5 6 8 10 4syl N0ℤRHomY:B
12 sseq1 =ifN=00..^NifN=00..^N
13 sseq1 0..^N=ifN=00..^N0..^NifN=00..^N
14 ssid
15 elfzoelz x0..^Nx
16 15 ssriv 0..^N
17 12 13 14 16 keephyp ifN=00..^N
18 4 17 eqsstri W
19 fssres ℤRHomY:BWℤRHomYW:WB
20 11 18 19 sylancl N0ℤRHomYW:WB
21 3 feq1i F:WBℤRHomYW:WB
22 20 21 sylibr N0F:WB
23 3 fveq1i Fx=ℤRHomYWx
24 fvres xWℤRHomYWx=ℤRHomYx
25 24 ad2antrl N0xWyWℤRHomYWx=ℤRHomYx
26 23 25 eqtrid N0xWyWFx=ℤRHomYx
27 3 fveq1i Fy=ℤRHomYWy
28 fvres yWℤRHomYWy=ℤRHomYy
29 28 ad2antll N0xWyWℤRHomYWy=ℤRHomYy
30 27 29 eqtrid N0xWyWFy=ℤRHomYy
31 26 30 eqeq12d N0xWyWFx=FyℤRHomYx=ℤRHomYy
32 simpl N0xWyWN0
33 simprl N0xWyWxW
34 18 33 sselid N0xWyWx
35 simprr N0xWyWyW
36 18 35 sselid N0xWyWy
37 1 7 zndvds N0xyℤRHomYx=ℤRHomYyNxy
38 32 34 36 37 syl3anc N0xWyWℤRHomYx=ℤRHomYyNxy
39 elnn0 N0NN=0
40 simpl NxWyWN
41 simprl NxWyWxW
42 18 41 sselid NxWyWx
43 simprr NxWyWyW
44 18 43 sselid NxWyWy
45 moddvds NxyxmodN=ymodNNxy
46 40 42 44 45 syl3anc NxWyWxmodN=ymodNNxy
47 42 zred NxWyWx
48 nnrp NN+
49 48 adantr NxWyWN+
50 nnne0 NN0
51 ifnefalse N0ifN=00..^N=0..^N
52 50 51 syl NifN=00..^N=0..^N
53 4 52 eqtrid NW=0..^N
54 53 adantr NxWyWW=0..^N
55 41 54 eleqtrd NxWyWx0..^N
56 elfzole1 x0..^N0x
57 55 56 syl NxWyW0x
58 elfzolt2 x0..^Nx<N
59 55 58 syl NxWyWx<N
60 modid xN+0xx<NxmodN=x
61 47 49 57 59 60 syl22anc NxWyWxmodN=x
62 44 zred NxWyWy
63 43 54 eleqtrd NxWyWy0..^N
64 elfzole1 y0..^N0y
65 63 64 syl NxWyW0y
66 elfzolt2 y0..^Ny<N
67 63 66 syl NxWyWy<N
68 modid yN+0yy<NymodN=y
69 62 49 65 67 68 syl22anc NxWyWymodN=y
70 61 69 eqeq12d NxWyWxmodN=ymodNx=y
71 46 70 bitr3d NxWyWNxyx=y
72 simpl N=0xWyWN=0
73 72 breq1d N=0xWyWNxy0xy
74 id N=0N=0
75 0nn0 00
76 74 75 eqeltrdi N=0N0
77 76 34 sylan N=0xWyWx
78 76 36 sylan N=0xWyWy
79 77 78 zsubcld N=0xWyWxy
80 0dvds xy0xyxy=0
81 79 80 syl N=0xWyW0xyxy=0
82 77 zcnd N=0xWyWx
83 78 zcnd N=0xWyWy
84 82 83 subeq0ad N=0xWyWxy=0x=y
85 73 81 84 3bitrd N=0xWyWNxyx=y
86 71 85 jaoian NN=0xWyWNxyx=y
87 39 86 sylanb N0xWyWNxyx=y
88 31 38 87 3bitrd N0xWyWFx=Fyx=y
89 88 biimpd N0xWyWFx=Fyx=y
90 89 ralrimivva N0xWyWFx=Fyx=y
91 dff13 F:W1-1BF:WBxWyWFx=Fyx=y
92 22 90 91 sylanbrc N0F:W1-1B
93 zmodfzo zNzmodN0..^N
94 93 ancoms NzzmodN0..^N
95 53 adantr NzW=0..^N
96 94 95 eleqtrrd NzzmodNW
97 zre zz
98 modabs2 zN+zmodNmodN=zmodN
99 97 48 98 syl2anr NzzmodNmodN=zmodN
100 simpl NzN
101 16 94 sselid NzzmodN
102 simpr Nzz
103 moddvds NzmodNzzmodNmodN=zmodNNzmodNz
104 100 101 102 103 syl3anc NzzmodNmodN=zmodNNzmodNz
105 99 104 mpbid NzNzmodNz
106 nnnn0 NN0
107 106 adantr NzN0
108 1 7 zndvds N0zmodNzℤRHomYzmodN=ℤRHomYzNzmodNz
109 107 101 102 108 syl3anc NzℤRHomYzmodN=ℤRHomYzNzmodNz
110 105 109 mpbird NzℤRHomYzmodN=ℤRHomYz
111 110 eqcomd NzℤRHomYz=ℤRHomYzmodN
112 fveq2 y=zmodNℤRHomYy=ℤRHomYzmodN
113 112 rspceeqv zmodNWℤRHomYz=ℤRHomYzmodNyWℤRHomYz=ℤRHomYy
114 96 111 113 syl2anc NzyWℤRHomYz=ℤRHomYy
115 iftrue N=0ifN=00..^N=
116 115 eleq2d N=0zifN=00..^Nz
117 116 biimpar N=0zzifN=00..^N
118 117 4 eleqtrrdi N=0zzW
119 eqidd N=0zℤRHomYz=ℤRHomYz
120 fveq2 y=zℤRHomYy=ℤRHomYz
121 120 rspceeqv zWℤRHomYz=ℤRHomYzyWℤRHomYz=ℤRHomYy
122 118 119 121 syl2anc N=0zyWℤRHomYz=ℤRHomYy
123 114 122 jaoian NN=0zyWℤRHomYz=ℤRHomYy
124 39 123 sylanb N0zyWℤRHomYz=ℤRHomYy
125 27 28 eqtrid yWFy=ℤRHomYy
126 125 eqeq2d yWℤRHomYz=FyℤRHomYz=ℤRHomYy
127 126 rexbiia yWℤRHomYz=FyyWℤRHomYz=ℤRHomYy
128 124 127 sylibr N0zyWℤRHomYz=Fy
129 128 ralrimiva N0zyWℤRHomYz=Fy
130 1 2 7 znzrhfo N0ℤRHomY:ontoB
131 fofn ℤRHomY:ontoBℤRHomYFn
132 eqeq1 x=ℤRHomYzx=FyℤRHomYz=Fy
133 132 rexbidv x=ℤRHomYzyWx=FyyWℤRHomYz=Fy
134 133 ralrn ℤRHomYFnxranℤRHomYyWx=FyzyWℤRHomYz=Fy
135 130 131 134 3syl N0xranℤRHomYyWx=FyzyWℤRHomYz=Fy
136 129 135 mpbird N0xranℤRHomYyWx=Fy
137 forn ℤRHomY:ontoBranℤRHomY=B
138 130 137 syl N0ranℤRHomY=B
139 138 raleqdv N0xranℤRHomYyWx=FyxByWx=Fy
140 136 139 mpbid N0xByWx=Fy
141 dffo3 F:WontoBF:WBxByWx=Fy
142 22 140 141 sylanbrc N0F:WontoB
143 df-f1o F:W1-1 ontoBF:W1-1BF:WontoB
144 92 142 143 sylanbrc N0F:W1-1 ontoB