Metamath Proof Explorer


Theorem poimirlem18

Description: Lemma for poimir stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (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
poimirlem22.2 φ T S
poimirlem18.3 φ n 1 N p ran F p n K
poimirlem18.4 φ 2 nd T = 0
Assertion poimirlem18 φ ∃! z S z T

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 poimirlem22.2 φ T S
5 poimirlem18.3 φ n 1 N p ran F p n K
6 poimirlem18.4 φ 2 nd T = 0
7 1 2 3 4 5 6 poimirlem17 φ z S z T
8 6 adantr φ z S 2 nd T = 0
9 0nnn ¬ 0
10 elfznn 0 1 N 1 0
11 9 10 mto ¬ 0 1 N 1
12 eleq1 2 nd z = 0 2 nd z 1 N 1 0 1 N 1
13 11 12 mtbiri 2 nd z = 0 ¬ 2 nd z 1 N 1
14 13 necon2ai 2 nd z 1 N 1 2 nd z 0
15 1 ad2antrr φ z S 2 nd z 1 N 1 N
16 fveq2 t = z 2 nd t = 2 nd z
17 16 breq2d t = z y < 2 nd t y < 2 nd z
18 17 ifbid t = z if y < 2 nd t y y + 1 = if y < 2 nd z y y + 1
19 18 csbeq1d t = z 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 = if y < 2 nd z 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
20 2fveq3 t = z 1 st 1 st t = 1 st 1 st z
21 2fveq3 t = z 2 nd 1 st t = 2 nd 1 st z
22 21 imaeq1d t = z 2 nd 1 st t 1 j = 2 nd 1 st z 1 j
23 22 xpeq1d t = z 2 nd 1 st t 1 j × 1 = 2 nd 1 st z 1 j × 1
24 21 imaeq1d t = z 2 nd 1 st t j + 1 N = 2 nd 1 st z j + 1 N
25 24 xpeq1d t = z 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st z j + 1 N × 0
26 23 25 uneq12d t = z 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
27 20 26 oveq12d t = z 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
28 27 csbeq2dv t = z if y < 2 nd z 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 = if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
29 19 28 eqtrd t = z 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 = if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
30 29 mpteq2dv t = z 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 = y 0 N 1 if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
31 30 eqeq2d t = z 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 F = y 0 N 1 if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
32 31 2 elrab2 z S z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N F = y 0 N 1 if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
33 32 simprbi z S F = y 0 N 1 if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
34 33 ad2antlr φ z S 2 nd z 1 N 1 F = y 0 N 1 if y < 2 nd z y y + 1 / j 1 st 1 st z + f 2 nd 1 st z 1 j × 1 2 nd 1 st z j + 1 N × 0
35 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
36 35 2 eleq2s z S z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
37 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
38 36 37 syl z S 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
39 xp1st 1 st z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st z 0 ..^ K 1 N
40 38 39 syl z S 1 st 1 st z 0 ..^ K 1 N
41 elmapi 1 st 1 st z 0 ..^ K 1 N 1 st 1 st z : 1 N 0 ..^ K
42 40 41 syl z S 1 st 1 st z : 1 N 0 ..^ K
43 elfzoelz n 0 ..^ K n
44 43 ssriv 0 ..^ K
45 fss 1 st 1 st z : 1 N 0 ..^ K 0 ..^ K 1 st 1 st z : 1 N
46 42 44 45 sylancl z S 1 st 1 st z : 1 N
47 46 ad2antlr φ z S 2 nd z 1 N 1 1 st 1 st z : 1 N
48 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
49 38 48 syl z S 2 nd 1 st z f | f : 1 N 1-1 onto 1 N
50 fvex 2 nd 1 st z V
51 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
52 50 51 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
53 49 52 sylib z S 2 nd 1 st z : 1 N 1-1 onto 1 N
54 53 ad2antlr φ z S 2 nd z 1 N 1 2 nd 1 st z : 1 N 1-1 onto 1 N
55 simpr φ z S 2 nd z 1 N 1 2 nd z 1 N 1
56 15 34 47 54 55 poimirlem1 φ z S 2 nd z 1 N 1 ¬ * n 1 N F 2 nd z 1 n F 2 nd z n
57 1 ad2antrr φ 2 nd z 1 N 1 2 nd T 2 nd z N
58 fveq2 t = T 2 nd t = 2 nd T
59 58 breq2d t = T y < 2 nd t y < 2 nd T
60 59 ifbid t = T if y < 2 nd t y y + 1 = if y < 2 nd T y y + 1
61 60 csbeq1d t = T 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 = 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
62 2fveq3 t = T 1 st 1 st t = 1 st 1 st T
63 2fveq3 t = T 2 nd 1 st t = 2 nd 1 st T
64 63 imaeq1d t = T 2 nd 1 st t 1 j = 2 nd 1 st T 1 j
65 64 xpeq1d t = T 2 nd 1 st t 1 j × 1 = 2 nd 1 st T 1 j × 1
66 63 imaeq1d t = T 2 nd 1 st t j + 1 N = 2 nd 1 st T j + 1 N
67 66 xpeq1d t = T 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T j + 1 N × 0
68 65 67 uneq12d t = T 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
69 62 68 oveq12d t = T 1 st 1 st t + f 2 nd 1 st t 1 j × 1 2 nd 1 st t j + 1 N × 0 = 1 st 1 st T + f 2 nd 1 st T 1 j × 1 2 nd 1 st T j + 1 N × 0
70 69 csbeq2dv t = T 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 = 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
71 61 70 eqtrd t = T 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 = 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
72 71 mpteq2dv t = T 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 = 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
73 72 eqeq2d t = T 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 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
74 73 2 elrab2 T 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
75 74 simprbi T S 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
76 4 75 syl φ 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
77 76 ad2antrr φ 2 nd z 1 N 1 2 nd T 2 nd z 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
78 elrabi T 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 T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
79 78 2 eleq2s T S T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
80 4 79 syl φ T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
81 xp1st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
82 80 81 syl φ 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
83 xp1st 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st 1 st T 0 ..^ K 1 N
84 82 83 syl φ 1 st 1 st T 0 ..^ K 1 N
85 elmapi 1 st 1 st T 0 ..^ K 1 N 1 st 1 st T : 1 N 0 ..^ K
86 84 85 syl φ 1 st 1 st T : 1 N 0 ..^ K
87 fss 1 st 1 st T : 1 N 0 ..^ K 0 ..^ K 1 st 1 st T : 1 N
88 86 44 87 sylancl φ 1 st 1 st T : 1 N
89 88 ad2antrr φ 2 nd z 1 N 1 2 nd T 2 nd z 1 st 1 st T : 1 N
90 xp2nd 1 st T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
91 82 90 syl φ 2 nd 1 st T f | f : 1 N 1-1 onto 1 N
92 fvex 2 nd 1 st T V
93 f1oeq1 f = 2 nd 1 st T f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
94 92 93 elab 2 nd 1 st T f | f : 1 N 1-1 onto 1 N 2 nd 1 st T : 1 N 1-1 onto 1 N
95 91 94 sylib φ 2 nd 1 st T : 1 N 1-1 onto 1 N
96 95 ad2antrr φ 2 nd z 1 N 1 2 nd T 2 nd z 2 nd 1 st T : 1 N 1-1 onto 1 N
97 simplr φ 2 nd z 1 N 1 2 nd T 2 nd z 2 nd z 1 N 1
98 xp2nd T 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd T 0 N
99 80 98 syl φ 2 nd T 0 N
100 99 adantr φ 2 nd z 1 N 1 2 nd T 0 N
101 eldifsn 2 nd T 0 N 2 nd z 2 nd T 0 N 2 nd T 2 nd z
102 101 biimpri 2 nd T 0 N 2 nd T 2 nd z 2 nd T 0 N 2 nd z
103 100 102 sylan φ 2 nd z 1 N 1 2 nd T 2 nd z 2 nd T 0 N 2 nd z
104 57 77 89 96 97 103 poimirlem2 φ 2 nd z 1 N 1 2 nd T 2 nd z * n 1 N F 2 nd z 1 n F 2 nd z n
105 104 ex φ 2 nd z 1 N 1 2 nd T 2 nd z * n 1 N F 2 nd z 1 n F 2 nd z n
106 105 necon1bd φ 2 nd z 1 N 1 ¬ * n 1 N F 2 nd z 1 n F 2 nd z n 2 nd T = 2 nd z
107 106 adantlr φ z S 2 nd z 1 N 1 ¬ * n 1 N F 2 nd z 1 n F 2 nd z n 2 nd T = 2 nd z
108 56 107 mpd φ z S 2 nd z 1 N 1 2 nd T = 2 nd z
109 108 neeq1d φ z S 2 nd z 1 N 1 2 nd T 0 2 nd z 0
110 109 exbiri φ z S 2 nd z 1 N 1 2 nd z 0 2 nd T 0
111 14 110 mpdi φ z S 2 nd z 1 N 1 2 nd T 0
112 111 necon2bd φ z S 2 nd T = 0 ¬ 2 nd z 1 N 1
113 8 112 mpd φ z S ¬ 2 nd z 1 N 1
114 xp2nd z 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd z 0 N
115 36 114 syl z S 2 nd z 0 N
116 1 nncnd φ N
117 npcan1 N N - 1 + 1 = N
118 116 117 syl φ N - 1 + 1 = N
119 nnuz = 1
120 1 119 eleqtrdi φ N 1
121 118 120 eqeltrd φ N - 1 + 1 1
122 1 nnzd φ N
123 peano2zm N N 1
124 122 123 syl φ N 1
125 uzid N 1 N 1 N 1
126 peano2uz N 1 N 1 N - 1 + 1 N 1
127 124 125 126 3syl φ N - 1 + 1 N 1
128 118 127 eqeltrrd φ N N 1
129 fzsplit2 N - 1 + 1 1 N N 1 1 N = 1 N 1 N - 1 + 1 N
130 121 128 129 syl2anc φ 1 N = 1 N 1 N - 1 + 1 N
131 118 oveq1d φ N - 1 + 1 N = N N
132 fzsn N N N = N
133 122 132 syl φ N N = N
134 131 133 eqtrd φ N - 1 + 1 N = N
135 134 uneq2d φ 1 N 1 N - 1 + 1 N = 1 N 1 N
136 130 135 eqtrd φ 1 N = 1 N 1 N
137 136 eleq2d φ 2 nd z 1 N 2 nd z 1 N 1 N
138 137 notbid φ ¬ 2 nd z 1 N ¬ 2 nd z 1 N 1 N
139 ioran ¬ 2 nd z 1 N 1 2 nd z = N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N
140 elun 2 nd z 1 N 1 N 2 nd z 1 N 1 2 nd z N
141 fvex 2 nd z V
142 141 elsn 2 nd z N 2 nd z = N
143 142 orbi2i 2 nd z 1 N 1 2 nd z N 2 nd z 1 N 1 2 nd z = N
144 140 143 bitri 2 nd z 1 N 1 N 2 nd z 1 N 1 2 nd z = N
145 139 144 xchnxbir ¬ 2 nd z 1 N 1 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N
146 138 145 bitrdi φ ¬ 2 nd z 1 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N
147 146 anbi2d φ 2 nd z 0 N ¬ 2 nd z 1 N 2 nd z 0 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N
148 1 nnnn0d φ N 0
149 nn0uz 0 = 0
150 148 149 eleqtrdi φ N 0
151 fzpred N 0 0 N = 0 0 + 1 N
152 150 151 syl φ 0 N = 0 0 + 1 N
153 152 difeq1d φ 0 N 1 N = 0 0 + 1 N 1 N
154 difun2 0 1 N 1 N = 0 1 N
155 0p1e1 0 + 1 = 1
156 155 oveq1i 0 + 1 N = 1 N
157 156 uneq2i 0 0 + 1 N = 0 1 N
158 157 difeq1i 0 0 + 1 N 1 N = 0 1 N 1 N
159 incom 0 1 N = 1 N 0
160 elfznn 0 1 N 0
161 9 160 mto ¬ 0 1 N
162 disjsn 1 N 0 = ¬ 0 1 N
163 161 162 mpbir 1 N 0 =
164 159 163 eqtri 0 1 N =
165 disj3 0 1 N = 0 = 0 1 N
166 164 165 mpbi 0 = 0 1 N
167 154 158 166 3eqtr4i 0 0 + 1 N 1 N = 0
168 153 167 eqtrdi φ 0 N 1 N = 0
169 168 eleq2d φ 2 nd z 0 N 1 N 2 nd z 0
170 eldif 2 nd z 0 N 1 N 2 nd z 0 N ¬ 2 nd z 1 N
171 141 elsn 2 nd z 0 2 nd z = 0
172 169 170 171 3bitr3g φ 2 nd z 0 N ¬ 2 nd z 1 N 2 nd z = 0
173 147 172 bitr3d φ 2 nd z 0 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N 2 nd z = 0
174 173 biimpd φ 2 nd z 0 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N 2 nd z = 0
175 174 expdimp φ 2 nd z 0 N ¬ 2 nd z 1 N 1 ¬ 2 nd z = N 2 nd z = 0
176 115 175 sylan2 φ z S ¬ 2 nd z 1 N 1 ¬ 2 nd z = N 2 nd z = 0
177 113 176 mpand φ z S ¬ 2 nd z = N 2 nd z = 0
178 1 2 3 poimirlem13 φ * z S 2 nd z = 0
179 fveqeq2 z = s 2 nd z = 0 2 nd s = 0
180 179 rmo4 * z S 2 nd z = 0 z S s S 2 nd z = 0 2 nd s = 0 z = s
181 178 180 sylib φ z S s S 2 nd z = 0 2 nd s = 0 z = s
182 181 r19.21bi φ z S s S 2 nd z = 0 2 nd s = 0 z = s
183 4 adantr φ z S T S
184 fveqeq2 s = T 2 nd s = 0 2 nd T = 0
185 184 anbi2d s = T 2 nd z = 0 2 nd s = 0 2 nd z = 0 2 nd T = 0
186 eqeq2 s = T z = s z = T
187 185 186 imbi12d s = T 2 nd z = 0 2 nd s = 0 z = s 2 nd z = 0 2 nd T = 0 z = T
188 187 rspccv s S 2 nd z = 0 2 nd s = 0 z = s T S 2 nd z = 0 2 nd T = 0 z = T
189 182 183 188 sylc φ z S 2 nd z = 0 2 nd T = 0 z = T
190 8 189 mpan2d φ z S 2 nd z = 0 z = T
191 177 190 syld φ z S ¬ 2 nd z = N z = T
192 191 necon1ad φ z S z T 2 nd z = N
193 192 ralrimiva φ z S z T 2 nd z = N
194 1 2 3 poimirlem14 φ * z S 2 nd z = N
195 rmoim z S z T 2 nd z = N * z S 2 nd z = N * z S z T
196 193 194 195 sylc φ * z S z T
197 reu5 ∃! z S z T z S z T * z S z T
198 7 196 197 sylanbrc φ ∃! z S z T