Metamath Proof Explorer


Theorem poimirlem21

Description: Lemma for poimir stating that, given a face not on a back face of the cube and a simplex in which it's opposite the final point of 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=t0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
poimirlem22.1 φF:0N10K1N
poimirlem22.2 φTS
poimirlem22.3 φn1NpranFpn0
poimirlem21.4 φ2ndT=N
Assertion poimirlem21 φ∃!zSzT

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 poimirlem22.1 φF:0N10K1N
4 poimirlem22.2 φTS
5 poimirlem22.3 φn1NpranFpn0
6 poimirlem21.4 φ2ndT=N
7 1 2 3 4 5 6 poimirlem20 φzSzT
8 6 adantr φzS2ndT=N
9 1 nnred φN
10 9 ltm1d φN1<N
11 nnm1nn0 NN10
12 1 11 syl φN10
13 12 nn0red φN1
14 13 9 ltnled φN1<N¬NN1
15 10 14 mpbid φ¬NN1
16 elfzle2 N1N1NN1
17 15 16 nsyl φ¬N1N1
18 eleq1 2ndz=N2ndz1N1N1N1
19 18 notbid 2ndz=N¬2ndz1N1¬N1N1
20 17 19 syl5ibrcom φ2ndz=N¬2ndz1N1
21 20 necon2ad φ2ndz1N12ndzN
22 21 adantr φzS2ndz1N12ndzN
23 1 ad2antrr φzS2ndz1N1N
24 fveq2 t=z2ndt=2ndz
25 24 breq2d t=zy<2ndty<2ndz
26 25 ifbid t=zify<2ndtyy+1=ify<2ndzyy+1
27 26 csbeq1d t=zify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndzyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
28 2fveq3 t=z1st1stt=1st1stz
29 2fveq3 t=z2nd1stt=2nd1stz
30 29 imaeq1d t=z2nd1stt1j=2nd1stz1j
31 30 xpeq1d t=z2nd1stt1j×1=2nd1stz1j×1
32 29 imaeq1d t=z2nd1sttj+1N=2nd1stzj+1N
33 32 xpeq1d t=z2nd1sttj+1N×0=2nd1stzj+1N×0
34 31 33 uneq12d t=z2nd1stt1j×12nd1sttj+1N×0=2nd1stz1j×12nd1stzj+1N×0
35 28 34 oveq12d t=z1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stz+f2nd1stz1j×12nd1stzj+1N×0
36 35 csbeq2dv t=zify<2ndzyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
37 27 36 eqtrd t=zify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
38 37 mpteq2dv t=zy0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
39 38 eqeq2d t=zF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
40 39 2 elrab2 zSz0..^K1N×f|f:1N1-1 onto1N×0NF=y0N1ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
41 40 simprbi zSF=y0N1ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
42 41 ad2antlr φzS2ndz1N1F=y0N1ify<2ndzyy+1/j1st1stz+f2nd1stz1j×12nd1stzj+1N×0
43 elrabi zt0..^K1N×f|f:1N1-1 onto1N×0N|F=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0z0..^K1N×f|f:1N1-1 onto1N×0N
44 43 2 eleq2s zSz0..^K1N×f|f:1N1-1 onto1N×0N
45 xp1st z0..^K1N×f|f:1N1-1 onto1N×0N1stz0..^K1N×f|f:1N1-1 onto1N
46 44 45 syl zS1stz0..^K1N×f|f:1N1-1 onto1N
47 xp1st 1stz0..^K1N×f|f:1N1-1 onto1N1st1stz0..^K1N
48 46 47 syl zS1st1stz0..^K1N
49 elmapi 1st1stz0..^K1N1st1stz:1N0..^K
50 48 49 syl zS1st1stz:1N0..^K
51 elfzoelz n0..^Kn
52 51 ssriv 0..^K
53 fss 1st1stz:1N0..^K0..^K1st1stz:1N
54 50 52 53 sylancl zS1st1stz:1N
55 54 ad2antlr φzS2ndz1N11st1stz:1N
56 xp2nd 1stz0..^K1N×f|f:1N1-1 onto1N2nd1stzf|f:1N1-1 onto1N
57 46 56 syl zS2nd1stzf|f:1N1-1 onto1N
58 fvex 2nd1stzV
59 f1oeq1 f=2nd1stzf:1N1-1 onto1N2nd1stz:1N1-1 onto1N
60 58 59 elab 2nd1stzf|f:1N1-1 onto1N2nd1stz:1N1-1 onto1N
61 57 60 sylib zS2nd1stz:1N1-1 onto1N
62 61 ad2antlr φzS2ndz1N12nd1stz:1N1-1 onto1N
63 simpr φzS2ndz1N12ndz1N1
64 23 42 55 62 63 poimirlem1 φzS2ndz1N1¬*n1NF2ndz1nF2ndzn
65 1 ad2antrr φ2ndz1N12ndT2ndzN
66 fveq2 t=T2ndt=2ndT
67 66 breq2d t=Ty<2ndty<2ndT
68 67 ifbid t=Tify<2ndtyy+1=ify<2ndTyy+1
69 68 csbeq1d t=Tify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
70 2fveq3 t=T1st1stt=1st1stT
71 2fveq3 t=T2nd1stt=2nd1stT
72 71 imaeq1d t=T2nd1stt1j=2nd1stT1j
73 72 xpeq1d t=T2nd1stt1j×1=2nd1stT1j×1
74 71 imaeq1d t=T2nd1sttj+1N=2nd1stTj+1N
75 74 xpeq1d t=T2nd1sttj+1N×0=2nd1stTj+1N×0
76 73 75 uneq12d t=T2nd1stt1j×12nd1sttj+1N×0=2nd1stT1j×12nd1stTj+1N×0
77 70 76 oveq12d t=T1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stT+f2nd1stT1j×12nd1stTj+1N×0
78 77 csbeq2dv t=Tify<2ndTyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
79 69 78 eqtrd t=Tify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
80 79 mpteq2dv t=Ty0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
81 80 eqeq2d t=TF=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0F=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
82 81 2 elrab2 TST0..^K1N×f|f:1N1-1 onto1N×0NF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
83 82 simprbi TSF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
84 4 83 syl φF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
85 84 ad2antrr φ2ndz1N12ndT2ndzF=y0N1ify<2ndTyy+1/j1st1stT+f2nd1stT1j×12nd1stTj+1N×0
86 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
87 86 2 eleq2s TST0..^K1N×f|f:1N1-1 onto1N×0N
88 4 87 syl φT0..^K1N×f|f:1N1-1 onto1N×0N
89 xp1st T0..^K1N×f|f:1N1-1 onto1N×0N1stT0..^K1N×f|f:1N1-1 onto1N
90 88 89 syl φ1stT0..^K1N×f|f:1N1-1 onto1N
91 xp1st 1stT0..^K1N×f|f:1N1-1 onto1N1st1stT0..^K1N
92 90 91 syl φ1st1stT0..^K1N
93 elmapi 1st1stT0..^K1N1st1stT:1N0..^K
94 92 93 syl φ1st1stT:1N0..^K
95 fss 1st1stT:1N0..^K0..^K1st1stT:1N
96 94 52 95 sylancl φ1st1stT:1N
97 96 ad2antrr φ2ndz1N12ndT2ndz1st1stT:1N
98 xp2nd 1stT0..^K1N×f|f:1N1-1 onto1N2nd1stTf|f:1N1-1 onto1N
99 90 98 syl φ2nd1stTf|f:1N1-1 onto1N
100 fvex 2nd1stTV
101 f1oeq1 f=2nd1stTf:1N1-1 onto1N2nd1stT:1N1-1 onto1N
102 100 101 elab 2nd1stTf|f:1N1-1 onto1N2nd1stT:1N1-1 onto1N
103 99 102 sylib φ2nd1stT:1N1-1 onto1N
104 103 ad2antrr φ2ndz1N12ndT2ndz2nd1stT:1N1-1 onto1N
105 simplr φ2ndz1N12ndT2ndz2ndz1N1
106 xp2nd T0..^K1N×f|f:1N1-1 onto1N×0N2ndT0N
107 88 106 syl φ2ndT0N
108 107 adantr φ2ndz1N12ndT0N
109 eldifsn 2ndT0N2ndz2ndT0N2ndT2ndz
110 109 biimpri 2ndT0N2ndT2ndz2ndT0N2ndz
111 108 110 sylan φ2ndz1N12ndT2ndz2ndT0N2ndz
112 65 85 97 104 105 111 poimirlem2 φ2ndz1N12ndT2ndz*n1NF2ndz1nF2ndzn
113 112 ex φ2ndz1N12ndT2ndz*n1NF2ndz1nF2ndzn
114 113 necon1bd φ2ndz1N1¬*n1NF2ndz1nF2ndzn2ndT=2ndz
115 114 adantlr φzS2ndz1N1¬*n1NF2ndz1nF2ndzn2ndT=2ndz
116 64 115 mpd φzS2ndz1N12ndT=2ndz
117 116 neeq1d φzS2ndz1N12ndTN2ndzN
118 117 exbiri φzS2ndz1N12ndzN2ndTN
119 22 118 mpdd φzS2ndz1N12ndTN
120 119 necon2bd φzS2ndT=N¬2ndz1N1
121 8 120 mpd φzS¬2ndz1N1
122 xp2nd z0..^K1N×f|f:1N1-1 onto1N×0N2ndz0N
123 44 122 syl zS2ndz0N
124 nn0uz 0=0
125 12 124 eleqtrdi φN10
126 fzpred N100N1=00+1N1
127 125 126 syl φ0N1=00+1N1
128 0p1e1 0+1=1
129 128 oveq1i 0+1N1=1N1
130 129 uneq2i 00+1N1=01N1
131 127 130 eqtrdi φ0N1=01N1
132 131 eleq2d φ2ndz0N12ndz01N1
133 132 notbid φ¬2ndz0N1¬2ndz01N1
134 ioran ¬2ndz=02ndz1N1¬2ndz=0¬2ndz1N1
135 elun 2ndz01N12ndz02ndz1N1
136 fvex 2ndzV
137 136 elsn 2ndz02ndz=0
138 137 orbi1i 2ndz02ndz1N12ndz=02ndz1N1
139 135 138 bitri 2ndz01N12ndz=02ndz1N1
140 134 139 xchnxbir ¬2ndz01N1¬2ndz=0¬2ndz1N1
141 133 140 bitrdi φ¬2ndz0N1¬2ndz=0¬2ndz1N1
142 141 anbi2d φ2ndz0N¬2ndz0N12ndz0N¬2ndz=0¬2ndz1N1
143 uncom 0N1N=N0N1
144 143 difeq1i 0N1N0N1=N0N10N1
145 difun2 N0N10N1=N0N1
146 144 145 eqtri 0N1N0N1=N0N1
147 1 nncnd φN
148 npcan1 NN-1+1=N
149 147 148 syl φN-1+1=N
150 1 nnnn0d φN0
151 150 124 eleqtrdi φN0
152 149 151 eqeltrd φN-1+10
153 12 nn0zd φN1
154 uzid N1N1N1
155 peano2uz N1N1N-1+1N1
156 153 154 155 3syl φN-1+1N1
157 149 156 eqeltrrd φNN1
158 fzsplit2 N-1+10NN10N=0N1N-1+1N
159 152 157 158 syl2anc φ0N=0N1N-1+1N
160 149 oveq1d φN-1+1N=NN
161 1 nnzd φN
162 fzsn NNN=N
163 161 162 syl φNN=N
164 160 163 eqtrd φN-1+1N=N
165 164 uneq2d φ0N1N-1+1N=0N1N
166 159 165 eqtrd φ0N=0N1N
167 166 difeq1d φ0N0N1=0N1N0N1
168 elfzle2 N0N1NN1
169 15 168 nsyl φ¬N0N1
170 incom 0N1N=N0N1
171 170 eqeq1i 0N1N=N0N1=
172 disjsn 0N1N=¬N0N1
173 disj3 N0N1=N=N0N1
174 171 172 173 3bitr3i ¬N0N1N=N0N1
175 169 174 sylib φN=N0N1
176 146 167 175 3eqtr4a φ0N0N1=N
177 176 eleq2d φ2ndz0N0N12ndzN
178 eldif 2ndz0N0N12ndz0N¬2ndz0N1
179 136 elsn 2ndzN2ndz=N
180 177 178 179 3bitr3g φ2ndz0N¬2ndz0N12ndz=N
181 142 180 bitr3d φ2ndz0N¬2ndz=0¬2ndz1N12ndz=N
182 181 biimpd φ2ndz0N¬2ndz=0¬2ndz1N12ndz=N
183 182 expdimp φ2ndz0N¬2ndz=0¬2ndz1N12ndz=N
184 123 183 sylan2 φzS¬2ndz=0¬2ndz1N12ndz=N
185 121 184 mpan2d φzS¬2ndz=02ndz=N
186 1 2 3 poimirlem14 φ*zS2ndz=N
187 fveqeq2 z=s2ndz=N2nds=N
188 187 rmo4 *zS2ndz=NzSsS2ndz=N2nds=Nz=s
189 186 188 sylib φzSsS2ndz=N2nds=Nz=s
190 189 r19.21bi φzSsS2ndz=N2nds=Nz=s
191 4 adantr φzSTS
192 fveqeq2 s=T2nds=N2ndT=N
193 192 anbi2d s=T2ndz=N2nds=N2ndz=N2ndT=N
194 eqeq2 s=Tz=sz=T
195 193 194 imbi12d s=T2ndz=N2nds=Nz=s2ndz=N2ndT=Nz=T
196 195 rspccv sS2ndz=N2nds=Nz=sTS2ndz=N2ndT=Nz=T
197 190 191 196 sylc φzS2ndz=N2ndT=Nz=T
198 8 197 mpan2d φzS2ndz=Nz=T
199 185 198 syld φzS¬2ndz=0z=T
200 199 necon1ad φzSzT2ndz=0
201 200 ralrimiva φzSzT2ndz=0
202 1 2 3 poimirlem13 φ*zS2ndz=0
203 rmoim zSzT2ndz=0*zS2ndz=0*zSzT
204 201 202 203 sylc φ*zSzT
205 reu5 ∃!zSzTzSzT*zSzT
206 7 204 205 sylanbrc φ∃!zSzT