Metamath Proof Explorer


Theorem poimirlem8

Description: Lemma for poimir , establishing that away from the opposite vertex the walks in poimirlem9 yield the same vertices. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φN
poimirlem22.s S=t0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
poimirlem9.1 φTS
poimirlem9.2 φ2ndT1N1
poimirlem9.3 φUS
Assertion poimirlem8 φ2nd1stU1N2ndT2ndT+1=2nd1stT1N2ndT2ndT+1

Proof

Step Hyp Ref Expression
1 poimir.0 φN
2 poimirlem22.s S=t0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
3 poimirlem9.1 φTS
4 poimirlem9.2 φ2ndT1N1
5 poimirlem9.3 φUS
6 elrabi Ut0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0U0..^K1N×f|f:1N1-1 onto1N×0N
7 6 2 eleq2s USU0..^K1N×f|f:1N1-1 onto1N×0N
8 5 7 syl φU0..^K1N×f|f:1N1-1 onto1N×0N
9 xp1st U0..^K1N×f|f:1N1-1 onto1N×0N1stU0..^K1N×f|f:1N1-1 onto1N
10 8 9 syl φ1stU0..^K1N×f|f:1N1-1 onto1N
11 xp2nd 1stU0..^K1N×f|f:1N1-1 onto1N2nd1stUf|f:1N1-1 onto1N
12 10 11 syl φ2nd1stUf|f:1N1-1 onto1N
13 fvex 2nd1stUV
14 f1oeq1 f=2nd1stUf:1N1-1 onto1N2nd1stU:1N1-1 onto1N
15 13 14 elab 2nd1stUf|f:1N1-1 onto1N2nd1stU:1N1-1 onto1N
16 12 15 sylib φ2nd1stU:1N1-1 onto1N
17 f1ofn 2nd1stU:1N1-1 onto1N2nd1stUFn1N
18 16 17 syl φ2nd1stUFn1N
19 difss 1N2ndT2ndT+11N
20 fnssres 2nd1stUFn1N1N2ndT2ndT+11N2nd1stU1N2ndT2ndT+1Fn1N2ndT2ndT+1
21 18 19 20 sylancl φ2nd1stU1N2ndT2ndT+1Fn1N2ndT2ndT+1
22 elrabi Tt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0T0..^K1N×f|f:1N1-1 onto1N×0N
23 22 2 eleq2s TST0..^K1N×f|f:1N1-1 onto1N×0N
24 3 23 syl φT0..^K1N×f|f:1N1-1 onto1N×0N
25 xp1st T0..^K1N×f|f:1N1-1 onto1N×0N1stT0..^K1N×f|f:1N1-1 onto1N
26 24 25 syl φ1stT0..^K1N×f|f:1N1-1 onto1N
27 xp2nd 1stT0..^K1N×f|f:1N1-1 onto1N2nd1stTf|f:1N1-1 onto1N
28 26 27 syl φ2nd1stTf|f:1N1-1 onto1N
29 fvex 2nd1stTV
30 f1oeq1 f=2nd1stTf:1N1-1 onto1N2nd1stT:1N1-1 onto1N
31 29 30 elab 2nd1stTf|f:1N1-1 onto1N2nd1stT:1N1-1 onto1N
32 28 31 sylib φ2nd1stT:1N1-1 onto1N
33 f1ofn 2nd1stT:1N1-1 onto1N2nd1stTFn1N
34 32 33 syl φ2nd1stTFn1N
35 fnssres 2nd1stTFn1N1N2ndT2ndT+11N2nd1stT1N2ndT2ndT+1Fn1N2ndT2ndT+1
36 34 19 35 sylancl φ2nd1stT1N2ndT2ndT+1Fn1N2ndT2ndT+1
37 fzp1elp1 2ndT1N12ndT+11N-1+1
38 4 37 syl φ2ndT+11N-1+1
39 1 nncnd φN
40 npcan1 NN-1+1=N
41 39 40 syl φN-1+1=N
42 41 oveq2d φ1N-1+1=1N
43 38 42 eleqtrd φ2ndT+11N
44 fzsplit 2ndT+11N1N=12ndT+12ndT+1+1N
45 43 44 syl φ1N=12ndT+12ndT+1+1N
46 45 difeq1d φ1N2ndT2ndT+1=12ndT+12ndT+1+1N2ndT2ndT+1
47 difundir 12ndT+12ndT+1+1N2ndT2ndT+1=12ndT+12ndT2ndT+12ndT+1+1N2ndT2ndT+1
48 elfznn 2ndT1N12ndT
49 4 48 syl φ2ndT
50 49 nncnd φ2ndT
51 npcan1 2ndT2ndT-1+1=2ndT
52 50 51 syl φ2ndT-1+1=2ndT
53 nnuz =1
54 49 53 eleqtrdi φ2ndT1
55 52 54 eqeltrd φ2ndT-1+11
56 49 nnzd φ2ndT
57 peano2zm 2ndT2ndT1
58 56 57 syl φ2ndT1
59 uzid 2ndT12ndT12ndT1
60 peano2uz 2ndT12ndT12ndT-1+12ndT1
61 58 59 60 3syl φ2ndT-1+12ndT1
62 52 61 eqeltrrd φ2ndT2ndT1
63 peano2uz 2ndT2ndT12ndT+12ndT1
64 62 63 syl φ2ndT+12ndT1
65 fzsplit2 2ndT-1+112ndT+12ndT112ndT+1=12ndT12ndT-1+12ndT+1
66 55 64 65 syl2anc φ12ndT+1=12ndT12ndT-1+12ndT+1
67 52 oveq1d φ2ndT-1+12ndT+1=2ndT2ndT+1
68 fzpr 2ndT2ndT2ndT+1=2ndT2ndT+1
69 56 68 syl φ2ndT2ndT+1=2ndT2ndT+1
70 67 69 eqtrd φ2ndT-1+12ndT+1=2ndT2ndT+1
71 70 uneq2d φ12ndT12ndT-1+12ndT+1=12ndT12ndT2ndT+1
72 66 71 eqtrd φ12ndT+1=12ndT12ndT2ndT+1
73 72 difeq1d φ12ndT+12ndT2ndT+1=12ndT12ndT2ndT+12ndT2ndT+1
74 49 nnred φ2ndT
75 74 ltm1d φ2ndT1<2ndT
76 58 zred φ2ndT1
77 76 74 ltnled φ2ndT1<2ndT¬2ndT2ndT1
78 75 77 mpbid φ¬2ndT2ndT1
79 elfzle2 2ndT12ndT12ndT2ndT1
80 78 79 nsyl φ¬2ndT12ndT1
81 difsn ¬2ndT12ndT112ndT12ndT=12ndT1
82 80 81 syl φ12ndT12ndT=12ndT1
83 peano2re 2ndT2ndT+1
84 74 83 syl φ2ndT+1
85 74 ltp1d φ2ndT<2ndT+1
86 76 74 84 75 85 lttrd φ2ndT1<2ndT+1
87 76 84 ltnled φ2ndT1<2ndT+1¬2ndT+12ndT1
88 86 87 mpbid φ¬2ndT+12ndT1
89 elfzle2 2ndT+112ndT12ndT+12ndT1
90 88 89 nsyl φ¬2ndT+112ndT1
91 difsn ¬2ndT+112ndT112ndT12ndT+1=12ndT1
92 90 91 syl φ12ndT12ndT+1=12ndT1
93 82 92 ineq12d φ12ndT12ndT12ndT12ndT+1=12ndT112ndT1
94 difun2 12ndT12ndT2ndT+12ndT2ndT+1=12ndT12ndT2ndT+1
95 df-pr 2ndT2ndT+1=2ndT2ndT+1
96 95 difeq2i 12ndT12ndT2ndT+1=12ndT12ndT2ndT+1
97 difundi 12ndT12ndT2ndT+1=12ndT12ndT12ndT12ndT+1
98 94 96 97 3eqtrri 12ndT12ndT12ndT12ndT+1=12ndT12ndT2ndT+12ndT2ndT+1
99 inidm 12ndT112ndT1=12ndT1
100 93 98 99 3eqtr3g φ12ndT12ndT2ndT+12ndT2ndT+1=12ndT1
101 73 100 eqtrd φ12ndT+12ndT2ndT+1=12ndT1
102 peano2re 2ndT+12ndT+1+1
103 84 102 syl φ2ndT+1+1
104 84 ltp1d φ2ndT+1<2ndT+1+1
105 74 84 103 85 104 lttrd φ2ndT<2ndT+1+1
106 74 103 ltnled φ2ndT<2ndT+1+1¬2ndT+1+12ndT
107 105 106 mpbid φ¬2ndT+1+12ndT
108 elfzle1 2ndT2ndT+1+1N2ndT+1+12ndT
109 107 108 nsyl φ¬2ndT2ndT+1+1N
110 difsn ¬2ndT2ndT+1+1N2ndT+1+1N2ndT=2ndT+1+1N
111 109 110 syl φ2ndT+1+1N2ndT=2ndT+1+1N
112 84 103 ltnled φ2ndT+1<2ndT+1+1¬2ndT+1+12ndT+1
113 104 112 mpbid φ¬2ndT+1+12ndT+1
114 elfzle1 2ndT+12ndT+1+1N2ndT+1+12ndT+1
115 113 114 nsyl φ¬2ndT+12ndT+1+1N
116 difsn ¬2ndT+12ndT+1+1N2ndT+1+1N2ndT+1=2ndT+1+1N
117 115 116 syl φ2ndT+1+1N2ndT+1=2ndT+1+1N
118 111 117 ineq12d φ2ndT+1+1N2ndT2ndT+1+1N2ndT+1=2ndT+1+1N2ndT+1+1N
119 95 difeq2i 2ndT+1+1N2ndT2ndT+1=2ndT+1+1N2ndT2ndT+1
120 difundi 2ndT+1+1N2ndT2ndT+1=2ndT+1+1N2ndT2ndT+1+1N2ndT+1
121 119 120 eqtr2i 2ndT+1+1N2ndT2ndT+1+1N2ndT+1=2ndT+1+1N2ndT2ndT+1
122 inidm 2ndT+1+1N2ndT+1+1N=2ndT+1+1N
123 118 121 122 3eqtr3g φ2ndT+1+1N2ndT2ndT+1=2ndT+1+1N
124 101 123 uneq12d φ12ndT+12ndT2ndT+12ndT+1+1N2ndT2ndT+1=12ndT12ndT+1+1N
125 47 124 eqtrid φ12ndT+12ndT+1+1N2ndT2ndT+1=12ndT12ndT+1+1N
126 46 125 eqtrd φ1N2ndT2ndT+1=12ndT12ndT+1+1N
127 126 eleq2d φk1N2ndT2ndT+1k12ndT12ndT+1+1N
128 elun k12ndT12ndT+1+1Nk12ndT1k2ndT+1+1N
129 127 128 bitrdi φk1N2ndT2ndT+1k12ndT1k2ndT+1+1N
130 129 biimpa φk1N2ndT2ndT+1k12ndT1k2ndT+1+1N
131 fveq2 t=T2ndt=2ndT
132 131 breq2d t=Ty<2ndty<2ndT
133 132 ifbid t=Tify<2ndtyy+1=ify<2ndTyy+1
134 133 csbeq1d t=Tify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
135 2fveq3 t=T1st1stt=1st1stT
136 2fveq3 t=T2nd1stt=2nd1stT
137 136 imaeq1d t=T2nd1stt1j=2nd1stT1j
138 137 xpeq1d t=T2nd1stt1j×1=2nd1stT1j×1
139 136 imaeq1d t=T2nd1sttj+1N=2nd1stTj+1N
140 139 xpeq1d t=T2nd1sttj+1N×0=2nd1stTj+1N×0
141 138 140 uneq12d t=T2nd1stt1j×12nd1sttj+1N×0=2nd1stT1j×12nd1stTj+1N×0
142 135 141 oveq12d t=T1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stT+f2nd1stT1j×12nd1stTj+1N×0
143 142 csbeq2dv t=Tify<2ndTyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
144 134 143 eqtrd t=Tify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
145 144 mpteq2dv t=Ty0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
146 145 eqeq2d t=TF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
147 146 2 elrab2 TST0..^K1N×f|f:1N1-1 onto1N×0NF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
148 147 simprbi TSF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
149 3 148 syl φF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
150 xp1st 1stT0..^K1N×f|f:1N1-1 onto1N1st1stT0..^K1N
151 26 150 syl φ1st1stT0..^K1N
152 elmapi 1st1stT0..^K1N1st1stT:1N0..^K
153 151 152 syl φ1st1stT:1N0..^K
154 elfzoelz n0..^Kn
155 154 ssriv 0..^K
156 fss 1st1stT:1N0..^K0..^K1st1stT:1N
157 153 155 156 sylancl φ1st1stT:1N
158 1 149 157 32 4 poimirlem1 φ¬*n1NF2ndT1nF2ndTn
159 1 adantr φ2ndU2ndTN
160 fveq2 t=U2ndt=2ndU
161 160 breq2d t=Uy<2ndty<2ndU
162 161 ifbid t=Uify<2ndtyy+1=ify<2ndUyy+1
163 162 csbeq1d t=Uify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndUyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
164 2fveq3 t=U1st1stt=1st1stU
165 2fveq3 t=U2nd1stt=2nd1stU
166 165 imaeq1d t=U2nd1stt1j=2nd1stU1j
167 166 xpeq1d t=U2nd1stt1j×1=2nd1stU1j×1
168 165 imaeq1d t=U2nd1sttj+1N=2nd1stUj+1N
169 168 xpeq1d t=U2nd1sttj+1N×0=2nd1stUj+1N×0
170 167 169 uneq12d t=U2nd1stt1j×12nd1sttj+1N×0=2nd1stU1j×12nd1stUj+1N×0
171 164 170 oveq12d t=U1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stU+f2nd1stU1j×12nd1stUj+1N×0
172 171 csbeq2dv t=Uify<2ndUyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
173 163 172 eqtrd t=Uify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
174 173 mpteq2dv t=Uy0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
175 174 eqeq2d t=UF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
176 175 2 elrab2 USU0..^K1N×f|f:1N1-1 onto1N×0NF=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
177 176 simprbi USF=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
178 5 177 syl φF=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
179 178 adantr φ2ndU2ndTF=y0N1ify<2ndUyy+1/j1st1stU+f2nd1stU1j×12nd1stUj+1N×0
180 xp1st 1stU0..^K1N×f|f:1N1-1 onto1N1st1stU0..^K1N
181 10 180 syl φ1st1stU0..^K1N
182 elmapi 1st1stU0..^K1N1st1stU:1N0..^K
183 181 182 syl φ1st1stU:1N0..^K
184 fss 1st1stU:1N0..^K0..^K1st1stU:1N
185 183 155 184 sylancl φ1st1stU:1N
186 185 adantr φ2ndU2ndT1st1stU:1N
187 16 adantr φ2ndU2ndT2nd1stU:1N1-1 onto1N
188 4 adantr φ2ndU2ndT2ndT1N1
189 xp2nd U0..^K1N×f|f:1N1-1 onto1N×0N2ndU0N
190 8 189 syl φ2ndU0N
191 eldifsn 2ndU0N2ndT2ndU0N2ndU2ndT
192 191 biimpri 2ndU0N2ndU2ndT2ndU0N2ndT
193 190 192 sylan φ2ndU2ndT2ndU0N2ndT
194 159 179 186 187 188 193 poimirlem2 φ2ndU2ndT*n1NF2ndT1nF2ndTn
195 194 ex φ2ndU2ndT*n1NF2ndT1nF2ndTn
196 195 necon1bd φ¬*n1NF2ndT1nF2ndTn2ndU=2ndT
197 158 196 mpd φ2ndU=2ndT
198 197 oveq1d φ2ndU1=2ndT1
199 198 oveq2d φ12ndU1=12ndT1
200 199 eleq2d φk12ndU1k12ndT1
201 200 biimpar φk12ndT1k12ndU1
202 1 adantr φk12ndU1N
203 5 adantr φk12ndU1US
204 197 4 eqeltrd φ2ndU1N1
205 204 adantr φk12ndU12ndU1N1
206 simpr φk12ndU1k12ndU1
207 202 2 203 205 206 poimirlem6 φk12ndU1ιn1N|Fk1nFkn=2nd1stUk
208 201 207 syldan φk12ndT1ιn1N|Fk1nFkn=2nd1stUk
209 1 adantr φk12ndT1N
210 3 adantr φk12ndT1TS
211 4 adantr φk12ndT12ndT1N1
212 simpr φk12ndT1k12ndT1
213 209 2 210 211 212 poimirlem6 φk12ndT1ιn1N|Fk1nFkn=2nd1stTk
214 208 213 eqtr3d φk12ndT12nd1stUk=2nd1stTk
215 197 oveq1d φ2ndU+1=2ndT+1
216 215 oveq1d φ2ndU+1+1=2ndT+1+1
217 216 oveq1d φ2ndU+1+1N=2ndT+1+1N
218 217 eleq2d φk2ndU+1+1Nk2ndT+1+1N
219 218 biimpar φk2ndT+1+1Nk2ndU+1+1N
220 1 adantr φk2ndU+1+1NN
221 5 adantr φk2ndU+1+1NUS
222 204 adantr φk2ndU+1+1N2ndU1N1
223 simpr φk2ndU+1+1Nk2ndU+1+1N
224 220 2 221 222 223 poimirlem7 φk2ndU+1+1Nιn1N|Fk2nFk1n=2nd1stUk
225 219 224 syldan φk2ndT+1+1Nιn1N|Fk2nFk1n=2nd1stUk
226 1 adantr φk2ndT+1+1NN
227 3 adantr φk2ndT+1+1NTS
228 4 adantr φk2ndT+1+1N2ndT1N1
229 simpr φk2ndT+1+1Nk2ndT+1+1N
230 226 2 227 228 229 poimirlem7 φk2ndT+1+1Nιn1N|Fk2nFk1n=2nd1stTk
231 225 230 eqtr3d φk2ndT+1+1N2nd1stUk=2nd1stTk
232 214 231 jaodan φk12ndT1k2ndT+1+1N2nd1stUk=2nd1stTk
233 130 232 syldan φk1N2ndT2ndT+12nd1stUk=2nd1stTk
234 fvres k1N2ndT2ndT+12nd1stU1N2ndT2ndT+1k=2nd1stUk
235 234 adantl φk1N2ndT2ndT+12nd1stU1N2ndT2ndT+1k=2nd1stUk
236 fvres k1N2ndT2ndT+12nd1stT1N2ndT2ndT+1k=2nd1stTk
237 236 adantl φk1N2ndT2ndT+12nd1stT1N2ndT2ndT+1k=2nd1stTk
238 233 235 237 3eqtr4d φk1N2ndT2ndT+12nd1stU1N2ndT2ndT+1k=2nd1stT1N2ndT2ndT+1k
239 21 36 238 eqfnfvd φ2nd1stU1N2ndT2ndT+1=2nd1stT1N2ndT2ndT+1