Metamath Proof Explorer


Theorem poimirlem13

Description: Lemma for poimir - for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
poimirlem22.1 φ F : 0 N 1 0 K 1 N
Assertion poimirlem13 φ * z S 2 nd z = 0

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem22.s S = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0
3 poimirlem22.1 φ F : 0 N 1 0 K 1 N
4 1 ad2antrr φ z S k S 2 nd z = 0 2 nd k = 0 N
5 3 ad2antrr φ z S k S 2 nd z = 0 2 nd k = 0 F : 0 N 1 0 K 1 N
6 simplrl φ z S k S 2 nd z = 0 2 nd k = 0 z S
7 simprl φ z S k S 2 nd z = 0 2 nd k = 0 2 nd z = 0
8 4 2 5 6 7 poimirlem10 φ z S k S 2 nd z = 0 2 nd k = 0 F N 1 f 1 N × 1 = 1 st 1 st z
9 simplrr φ z S k S 2 nd z = 0 2 nd k = 0 k S
10 simprr φ z S k S 2 nd z = 0 2 nd k = 0 2 nd k = 0
11 4 2 5 9 10 poimirlem10 φ z S k S 2 nd z = 0 2 nd k = 0 F N 1 f 1 N × 1 = 1 st 1 st k
12 8 11 eqtr3d φ z S k S 2 nd z = 0 2 nd k = 0 1 st 1 st z = 1 st 1 st k
13 elrabi z t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
14 13 2 eleq2s z S z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
15 xp1st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
16 14 15 syl z S 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
17 xp2nd 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st z f | f : 1 N 1-1 onto 1 N
18 16 17 syl z S 2 nd 1 st z f | f : 1 N 1-1 onto 1 N
19 fvex 2 nd 1 st z V
20 f1oeq1 f = 2 nd 1 st z f : 1 N 1-1 onto 1 N 2 nd 1 st z : 1 N 1-1 onto 1 N
21 19 20 elab 2 nd 1 st z f | f : 1 N 1-1 onto 1 N 2 nd 1 st z : 1 N 1-1 onto 1 N
22 18 21 sylib z S 2 nd 1 st z : 1 N 1-1 onto 1 N
23 f1ofn 2 nd 1 st z : 1 N 1-1 onto 1 N 2 nd 1 st z Fn 1 N
24 22 23 syl z S 2 nd 1 st z Fn 1 N
25 24 adantr z S k S 2 nd 1 st z Fn 1 N
26 25 ad2antlr φ z S k S 2 nd z = 0 2 nd k = 0 2 nd 1 st z Fn 1 N
27 elrabi k t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | F = y 0 N 1 if y < 2 nd t y y + 1 / j 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
28 27 2 eleq2s k S k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
29 xp1st k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
30 28 29 syl k S 1 st k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
31 xp2nd 1 st k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st k f | f : 1 N 1-1 onto 1 N
32 30 31 syl k S 2 nd 1 st k f | f : 1 N 1-1 onto 1 N
33 fvex 2 nd 1 st k V
34 f1oeq1 f = 2 nd 1 st k f : 1 N 1-1 onto 1 N 2 nd 1 st k : 1 N 1-1 onto 1 N
35 33 34 elab 2 nd 1 st k f | f : 1 N 1-1 onto 1 N 2 nd 1 st k : 1 N 1-1 onto 1 N
36 32 35 sylib k S 2 nd 1 st k : 1 N 1-1 onto 1 N
37 f1ofn 2 nd 1 st k : 1 N 1-1 onto 1 N 2 nd 1 st k Fn 1 N
38 36 37 syl k S 2 nd 1 st k Fn 1 N
39 38 adantl z S k S 2 nd 1 st k Fn 1 N
40 39 ad2antlr φ z S k S 2 nd z = 0 2 nd k = 0 2 nd 1 st k Fn 1 N
41 eleq1 m = n m 1 N n 1 N
42 41 anbi2d m = n φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N
43 oveq2 m = n 1 m = 1 n
44 43 imaeq2d m = n 2 nd 1 st z 1 m = 2 nd 1 st z 1 n
45 43 imaeq2d m = n 2 nd 1 st k 1 m = 2 nd 1 st k 1 n
46 44 45 eqeq12d m = n 2 nd 1 st z 1 m = 2 nd 1 st k 1 m 2 nd 1 st z 1 n = 2 nd 1 st k 1 n
47 42 46 imbi12d m = n φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd 1 st z 1 m = 2 nd 1 st k 1 m φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z 1 n = 2 nd 1 st k 1 n
48 1 ad3antrrr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N N
49 3 ad3antrrr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N F : 0 N 1 0 K 1 N
50 simpl z S k S z S
51 50 ad3antlr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N z S
52 simplrl φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd z = 0
53 simpr z S k S k S
54 53 ad3antlr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N k S
55 simplrr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd k = 0
56 simpr φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N m 1 N
57 48 2 49 51 52 54 55 56 poimirlem11 φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd 1 st z 1 m 2 nd 1 st k 1 m
58 48 2 49 54 55 51 52 56 poimirlem11 φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd 1 st k 1 m 2 nd 1 st z 1 m
59 57 58 eqssd φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd 1 st z 1 m = 2 nd 1 st k 1 m
60 47 59 chvarvv φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z 1 n = 2 nd 1 st k 1 n
61 simpll φ z S k S 2 nd z = 0 2 nd k = 0 φ
62 elfznn n 1 N n
63 nnm1nn0 n n 1 0
64 62 63 syl n 1 N n 1 0
65 64 adantr n 1 N ¬ n = 1 n 1 0
66 62 nncnd n 1 N n
67 ax-1cn 1
68 subeq0 n 1 n 1 = 0 n = 1
69 66 67 68 sylancl n 1 N n 1 = 0 n = 1
70 69 necon3abid n 1 N n 1 0 ¬ n = 1
71 70 biimpar n 1 N ¬ n = 1 n 1 0
72 elnnne0 n 1 n 1 0 n 1 0
73 65 71 72 sylanbrc n 1 N ¬ n = 1 n 1
74 73 adantl φ n 1 N ¬ n = 1 n 1
75 64 nn0red n 1 N n 1
76 75 adantl φ n 1 N n 1
77 62 nnred n 1 N n
78 77 adantl φ n 1 N n
79 1 nnred φ N
80 79 adantr φ n 1 N N
81 77 lem1d n 1 N n 1 n
82 81 adantl φ n 1 N n 1 n
83 elfzle2 n 1 N n N
84 83 adantl φ n 1 N n N
85 76 78 80 82 84 letrd φ n 1 N n 1 N
86 85 adantrr φ n 1 N ¬ n = 1 n 1 N
87 1 nnzd φ N
88 fznn N n 1 1 N n 1 n 1 N
89 87 88 syl φ n 1 1 N n 1 n 1 N
90 89 adantr φ n 1 N ¬ n = 1 n 1 1 N n 1 n 1 N
91 74 86 90 mpbir2and φ n 1 N ¬ n = 1 n 1 1 N
92 61 91 sylan φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N ¬ n = 1 n 1 1 N
93 ovex n 1 V
94 eleq1 m = n 1 m 1 N n 1 1 N
95 94 anbi2d m = n 1 φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N φ z S k S 2 nd z = 0 2 nd k = 0 n 1 1 N
96 oveq2 m = n 1 1 m = 1 n 1
97 96 imaeq2d m = n 1 2 nd 1 st z 1 m = 2 nd 1 st z 1 n 1
98 96 imaeq2d m = n 1 2 nd 1 st k 1 m = 2 nd 1 st k 1 n 1
99 97 98 eqeq12d m = n 1 2 nd 1 st z 1 m = 2 nd 1 st k 1 m 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
100 95 99 imbi12d m = n 1 φ z S k S 2 nd z = 0 2 nd k = 0 m 1 N 2 nd 1 st z 1 m = 2 nd 1 st k 1 m φ z S k S 2 nd z = 0 2 nd k = 0 n 1 1 N 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
101 93 100 59 vtocl φ z S k S 2 nd z = 0 2 nd k = 0 n 1 1 N 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
102 92 101 syldan φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N ¬ n = 1 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
103 102 expr φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N ¬ n = 1 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
104 ima0 2 nd 1 st z =
105 ima0 2 nd 1 st k =
106 104 105 eqtr4i 2 nd 1 st z = 2 nd 1 st k
107 oveq1 n = 1 n 1 = 1 1
108 1m1e0 1 1 = 0
109 107 108 eqtrdi n = 1 n 1 = 0
110 109 oveq2d n = 1 1 n 1 = 1 0
111 fz10 1 0 =
112 110 111 eqtrdi n = 1 1 n 1 =
113 112 imaeq2d n = 1 2 nd 1 st z 1 n 1 = 2 nd 1 st z
114 112 imaeq2d n = 1 2 nd 1 st k 1 n 1 = 2 nd 1 st k
115 106 113 114 3eqtr4a n = 1 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
116 103 115 pm2.61d2 φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
117 60 116 difeq12d φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
118 fnsnfv 2 nd 1 st z Fn 1 N n 1 N 2 nd 1 st z n = 2 nd 1 st z n
119 24 118 sylan z S n 1 N 2 nd 1 st z n = 2 nd 1 st z n
120 62 adantl z S n 1 N n
121 uncom 1 n 1 n = n 1 n 1
122 121 difeq1i 1 n 1 n 1 n 1 = n 1 n 1 1 n 1
123 difun2 n 1 n 1 1 n 1 = n 1 n 1
124 122 123 eqtri 1 n 1 n 1 n 1 = n 1 n 1
125 nncn n n
126 npcan1 n n - 1 + 1 = n
127 125 126 syl n n - 1 + 1 = n
128 elnnuz n n 1
129 128 biimpi n n 1
130 127 129 eqeltrd n n - 1 + 1 1
131 63 nn0zd n n 1
132 uzid n 1 n 1 n 1
133 131 132 syl n n 1 n 1
134 peano2uz n 1 n 1 n - 1 + 1 n 1
135 133 134 syl n n - 1 + 1 n 1
136 127 135 eqeltrrd n n n 1
137 fzsplit2 n - 1 + 1 1 n n 1 1 n = 1 n 1 n - 1 + 1 n
138 130 136 137 syl2anc n 1 n = 1 n 1 n - 1 + 1 n
139 127 oveq1d n n - 1 + 1 n = n n
140 nnz n n
141 fzsn n n n = n
142 140 141 syl n n n = n
143 139 142 eqtrd n n - 1 + 1 n = n
144 143 uneq2d n 1 n 1 n - 1 + 1 n = 1 n 1 n
145 138 144 eqtrd n 1 n = 1 n 1 n
146 145 difeq1d n 1 n 1 n 1 = 1 n 1 n 1 n 1
147 nnre n n
148 ltm1 n n 1 < n
149 peano2rem n n 1
150 ltnle n 1 n n 1 < n ¬ n n 1
151 149 150 mpancom n n 1 < n ¬ n n 1
152 148 151 mpbid n ¬ n n 1
153 elfzle2 n 1 n 1 n n 1
154 152 153 nsyl n ¬ n 1 n 1
155 147 154 syl n ¬ n 1 n 1
156 incom 1 n 1 n = n 1 n 1
157 156 eqeq1i 1 n 1 n = n 1 n 1 =
158 disjsn 1 n 1 n = ¬ n 1 n 1
159 disj3 n 1 n 1 = n = n 1 n 1
160 157 158 159 3bitr3i ¬ n 1 n 1 n = n 1 n 1
161 155 160 sylib n n = n 1 n 1
162 124 146 161 3eqtr4a n 1 n 1 n 1 = n
163 120 162 syl z S n 1 N 1 n 1 n 1 = n
164 163 imaeq2d z S n 1 N 2 nd 1 st z 1 n 1 n 1 = 2 nd 1 st z n
165 dff1o3 2 nd 1 st z : 1 N 1-1 onto 1 N 2 nd 1 st z : 1 N onto 1 N Fun 2 nd 1 st z -1
166 165 simprbi 2 nd 1 st z : 1 N 1-1 onto 1 N Fun 2 nd 1 st z -1
167 22 166 syl z S Fun 2 nd 1 st z -1
168 imadif Fun 2 nd 1 st z -1 2 nd 1 st z 1 n 1 n 1 = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1
169 167 168 syl z S 2 nd 1 st z 1 n 1 n 1 = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1
170 169 adantr z S n 1 N 2 nd 1 st z 1 n 1 n 1 = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1
171 119 164 170 3eqtr2d z S n 1 N 2 nd 1 st z n = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1
172 6 171 sylan φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z n = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1
173 eleq1 z = k z S k S
174 173 anbi1d z = k z S n 1 N k S n 1 N
175 2fveq3 z = k 2 nd 1 st z = 2 nd 1 st k
176 175 fveq1d z = k 2 nd 1 st z n = 2 nd 1 st k n
177 176 sneqd z = k 2 nd 1 st z n = 2 nd 1 st k n
178 175 imaeq1d z = k 2 nd 1 st z 1 n = 2 nd 1 st k 1 n
179 175 imaeq1d z = k 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 1
180 178 179 difeq12d z = k 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1 = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
181 177 180 eqeq12d z = k 2 nd 1 st z n = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1 2 nd 1 st k n = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
182 174 181 imbi12d z = k z S n 1 N 2 nd 1 st z n = 2 nd 1 st z 1 n 2 nd 1 st z 1 n 1 k S n 1 N 2 nd 1 st k n = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
183 182 171 chvarvv k S n 1 N 2 nd 1 st k n = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
184 9 183 sylan φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st k n = 2 nd 1 st k 1 n 2 nd 1 st k 1 n 1
185 117 172 184 3eqtr4d φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z n = 2 nd 1 st k n
186 fvex 2 nd 1 st z n V
187 186 sneqr 2 nd 1 st z n = 2 nd 1 st k n 2 nd 1 st z n = 2 nd 1 st k n
188 185 187 syl φ z S k S 2 nd z = 0 2 nd k = 0 n 1 N 2 nd 1 st z n = 2 nd 1 st k n
189 26 40 188 eqfnfvd φ z S k S 2 nd z = 0 2 nd k = 0 2 nd 1 st z = 2 nd 1 st k
190 xpopth 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st z = 1 st 1 st k 2 nd 1 st z = 2 nd 1 st k 1 st z = 1 st k
191 16 30 190 syl2an z S k S 1 st 1 st z = 1 st 1 st k 2 nd 1 st z = 2 nd 1 st k 1 st z = 1 st k
192 191 ad2antlr φ z S k S 2 nd z = 0 2 nd k = 0 1 st 1 st z = 1 st 1 st k 2 nd 1 st z = 2 nd 1 st k 1 st z = 1 st k
193 12 189 192 mpbi2and φ z S k S 2 nd z = 0 2 nd k = 0 1 st z = 1 st k
194 eqtr3 2 nd z = 0 2 nd k = 0 2 nd z = 2 nd k
195 194 adantl φ z S k S 2 nd z = 0 2 nd k = 0 2 nd z = 2 nd k
196 xpopth z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N k 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st z = 1 st k 2 nd z = 2 nd k z = k
197 14 28 196 syl2an z S k S 1 st z = 1 st k 2 nd z = 2 nd k z = k
198 197 ad2antlr φ z S k S 2 nd z = 0 2 nd k = 0 1 st z = 1 st k 2 nd z = 2 nd k z = k
199 193 195 198 mpbi2and φ z S k S 2 nd z = 0 2 nd k = 0 z = k
200 199 ex φ z S k S 2 nd z = 0 2 nd k = 0 z = k
201 200 ralrimivva φ z S k S 2 nd z = 0 2 nd k = 0 z = k
202 fveqeq2 z = k 2 nd z = 0 2 nd k = 0
203 202 rmo4 * z S 2 nd z = 0 z S k S 2 nd z = 0 2 nd k = 0 z = k
204 201 203 sylibr φ * z S 2 nd z = 0