poimirlem22 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem22		Structured version Unicode version

Theorem poimirlem22 31870

Description: Lemma for poimir 31881, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem22.2
poimirlem22.3	$/\$
poimirlem22.4	$/\$

**Assertion**
Ref	Expression
poimirlem22

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem22**
Step	Hyp	Ref	Expression
1		poimir.0	. . . . 5
2	1	adantr 466	. . . 4 $/\$
3		poimirlem22.s	. . . 4 ..^
4		poimirlem22.1	. . . . 5
5	4	adantr 466	. . . 4 $/\$
6		poimirlem22.2	. . . . 5
7	6	adantr 466	. . . 4 $/\$
8		simpr 462	. . . 4 $/\$
9	2, 3, 5, 7, 8	poimirlem15 31863	. . 3 $/\$ $\$
10		fveq2 5873	. . . . . . . . . . . . . . . . . . . . . . . 24
11	10	breq2d 4429	. . . . . . . . . . . . . . . . . . . . . . 23
12	11	ifbid 3928	. . . . . . . . . . . . . . . . . . . . . 22
13	12	csbeq1d 3399	. . . . . . . . . . . . . . . . . . . . 21
14		fveq2 5873	. . . . . . . . . . . . . . . . . . . . . . . 24
15	14	fveq2d 5877	. . . . . . . . . . . . . . . . . . . . . . 23
16	14	fveq2d 5877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	16	imaeq1d 5179	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . . . . 24
19	16	imaeq1d 5179	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . . . . 24
21	18, 20	uneq12d 3618	. . . . . . . . . . . . . . . . . . . . . . 23
22	15, 21	oveq12d 6315	. . . . . . . . . . . . . . . . . . . . . 22
23	22	csbeq2dv 3806	. . . . . . . . . . . . . . . . . . . . 21
24	13, 23	eqtrd 2461	. . . . . . . . . . . . . . . . . . . 20
25	24	mpteq2dv 4505	. . . . . . . . . . . . . . . . . . 19
26	25	eqeq2d 2434	. . . . . . . . . . . . . . . . . 18
27	26, 3	elrab2 3228	. . . . . . . . . . . . . . . . 17 ..^ $/\$
28	27	simprbi 465	. . . . . . . . . . . . . . . 16
29	6, 28	syl 17	. . . . . . . . . . . . . . 15
30	29	adantr 466	. . . . . . . . . . . . . 14 $/\$
31		elrabi 3223	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
32	31, 3	eleq2s 2528	. . . . . . . . . . . . . . . . . . . 20 ..^
33	6, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
34		xp1st 6829	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
36		xp1st 6829	. . . . . . . . . . . . . . . . . 18 ..^ ..^
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ..^
38		elmapi 7493	. . . . . . . . . . . . . . . . 17 ..^ ..^
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ..^
40		elfzoelz 11914	. . . . . . . . . . . . . . . . 17 ..^
41	40	ssriv 3465	. . . . . . . . . . . . . . . 16 ..^
42		fss 5746	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
43	39, 41, 42	sylancl 666	. . . . . . . . . . . . . . 15
44	43	adantr 466	. . . . . . . . . . . . . 14 $/\$
45		xp2nd 6830	. . . . . . . . . . . . . . . . 17 ..^
46	35, 45	syl 17	. . . . . . . . . . . . . . . 16
47		fvex 5883	. . . . . . . . . . . . . . . . 17
48		f1oeq1 5814	. . . . . . . . . . . . . . . . 17
49	47, 48	elab 3215	. . . . . . . . . . . . . . . 16
50	46, 49	sylib 199	. . . . . . . . . . . . . . 15
51	50	adantr 466	. . . . . . . . . . . . . 14 $/\$
52	2, 30, 44, 51, 8	poimirlem1 31849	. . . . . . . . . . . . 13 $/\$
53	52	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$
54	1	ad3antrrr 734	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
55		fveq2 5873	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	breq2d 4429	. . . . . . . . . . . . . . . . . . . . . . 23
57	56	ifbid 3928	. . . . . . . . . . . . . . . . . . . . . 22
58	57	csbeq1d 3399	. . . . . . . . . . . . . . . . . . . . 21
59		fveq2 5873	. . . . . . . . . . . . . . . . . . . . . . . 24
60	59	fveq2d 5877	. . . . . . . . . . . . . . . . . . . . . . 23
61	59	fveq2d 5877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	61	imaeq1d 5179	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	62	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . . . . 24
64	61	imaeq1d 5179	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	64	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . . . . 24
66	63, 65	uneq12d 3618	. . . . . . . . . . . . . . . . . . . . . . 23
67	60, 66	oveq12d 6315	. . . . . . . . . . . . . . . . . . . . . 22
68	67	csbeq2dv 3806	. . . . . . . . . . . . . . . . . . . . 21
69	58, 68	eqtrd 2461	. . . . . . . . . . . . . . . . . . . 20
70	69	mpteq2dv 4505	. . . . . . . . . . . . . . . . . . 19
71	70	eqeq2d 2434	. . . . . . . . . . . . . . . . . 18
72	71, 3	elrab2 3228	. . . . . . . . . . . . . . . . 17 ..^ $/\$
73	72	simprbi 465	. . . . . . . . . . . . . . . 16
74	73	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		elrabi 3223	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
76	75, 3	eleq2s 2528	. . . . . . . . . . . . . . . . . . . 20 ..^
77		xp1st 6829	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
79		xp1st 6829	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
81		elmapi 7493	. . . . . . . . . . . . . . . . . 18 ..^ ..^
82	80, 81	syl 17	. . . . . . . . . . . . . . . . 17 ..^
83		fss 5746	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
84	82, 41, 83	sylancl 666	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86		xp2nd 6830	. . . . . . . . . . . . . . . . . 18 ..^
87	78, 86	syl 17	. . . . . . . . . . . . . . . . 17
88		fvex 5883	. . . . . . . . . . . . . . . . . 18
89		f1oeq1 5814	. . . . . . . . . . . . . . . . . 18
90	88, 89	elab 3215	. . . . . . . . . . . . . . . . 17
91	87, 90	sylib 199	. . . . . . . . . . . . . . . 16
92	91	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93		simpllr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94		xp2nd 6830	. . . . . . . . . . . . . . . . . 18 ..^
95	76, 94	syl 17	. . . . . . . . . . . . . . . . 17
96	95	adantl 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97		eldifsn 4119	. . . . . . . . . . . . . . . . 17 $\$ $/\$
98	97	biimpri 209	. . . . . . . . . . . . . . . 16 $/\$ $\$
99	96, 98	sylan 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
100	54, 74, 85, 92, 93, 99	poimirlem2 31850	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100	ex 435	. . . . . . . . . . . . 13 $/\$ $/\$
102	101	necon1bd 2640	. . . . . . . . . . . 12 $/\$ $/\$
103	53, 102	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
104		eleq1 2492	. . . . . . . . . . . . . . . 16
105	104	biimparc 489	. . . . . . . . . . . . . . 15 $/\$
106	105	anim2i 571	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	106	anassrs 652	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	73	adantl 467	. . . . . . . . . . . . . 14 $/\$ $/\$
109		breq1 4420	. . . . . . . . . . . . . . . . . 18
110		id 23	. . . . . . . . . . . . . . . . . 18
111	109, 110	ifbieq1d 3929	. . . . . . . . . . . . . . . . 17
112		elfznn 11822	. . . . . . . . . . . . . . . . . . . 20
113	112	nngt0d 10649	. . . . . . . . . . . . . . . . . . 19
114	113	iftrued 3914	. . . . . . . . . . . . . . . . . 18
115	114	ad2antlr 731	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	111, 115	sylan9eqr 2483	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117	116	csbeq1d 3399	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
118		c0ex 9633	. . . . . . . . . . . . . . . . . 18
119		oveq2 6305	. . . . . . . . . . . . . . . . . . . . . . . 24
120		fz10 11814	. . . . . . . . . . . . . . . . . . . . . . . 24
121	119, 120	syl6eq 2477	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	imaeq2d 5180	. . . . . . . . . . . . . . . . . . . . . 22
123	122	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . 21
124		oveq1 6304	. . . . . . . . . . . . . . . . . . . . . . . . 25
125		0p1e1 10717	. . . . . . . . . . . . . . . . . . . . . . . . 25
126	124, 125	syl6eq 2477	. . . . . . . . . . . . . . . . . . . . . . . 24
127	126	oveq1d 6312	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	imaeq2d 5180	. . . . . . . . . . . . . . . . . . . . . 22
129	128	xpeq1d 4869	. . . . . . . . . . . . . . . . . . . . 21
130	123, 129	uneq12d 3618	. . . . . . . . . . . . . . . . . . . 20
131		ima0 5195	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	xpeq1i 4866	. . . . . . . . . . . . . . . . . . . . . . 23
133		0xp 4927	. . . . . . . . . . . . . . . . . . . . . . 23
134	132, 133	eqtri 2449	. . . . . . . . . . . . . . . . . . . . . 22
135	134	uneq1i 3613	. . . . . . . . . . . . . . . . . . . . 21
136		uncom 3607	. . . . . . . . . . . . . . . . . . . . 21
137		un0 3784	. . . . . . . . . . . . . . . . . . . . 21
138	135, 136, 137	3eqtri 2453	. . . . . . . . . . . . . . . . . . . 20
139	130, 138	syl6eq 2477	. . . . . . . . . . . . . . . . . . 19
140	139	oveq2d 6313	. . . . . . . . . . . . . . . . . 18
141	118, 140	csbie 3418	. . . . . . . . . . . . . . . . 17
142		f1ofo 5830	. . . . . . . . . . . . . . . . . . . . . 22
143	91, 142	syl 17	. . . . . . . . . . . . . . . . . . . . 21
144		foima 5807	. . . . . . . . . . . . . . . . . . . . 21
145	143, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20
146	145	xpeq1d 4869	. . . . . . . . . . . . . . . . . . 19
147	146	oveq2d 6313	. . . . . . . . . . . . . . . . . 18
148		ovex 6325	. . . . . . . . . . . . . . . . . . . 20
149	148	a1i 11	. . . . . . . . . . . . . . . . . . 19
150		ffn 5738	. . . . . . . . . . . . . . . . . . . 20 ..^
151	82, 150	syl 17	. . . . . . . . . . . . . . . . . . 19
152		fnconstg 5780	. . . . . . . . . . . . . . . . . . . 20
153	118, 152	mp1i 13	. . . . . . . . . . . . . . . . . . 19
154		eqidd 2421	. . . . . . . . . . . . . . . . . . 19 $/\$
155	118	fvconst2 6127	. . . . . . . . . . . . . . . . . . . 20
156	155	adantl 467	. . . . . . . . . . . . . . . . . . 19 $/\$
157	82	ffvelrnda 6029	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
158		elfzonn0 11954	. . . . . . . . . . . . . . . . . . . . . 22 ..^
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
160	159	nn0cnd 10923	. . . . . . . . . . . . . . . . . . . 20 $/\$
161	160	addid1d 9829	. . . . . . . . . . . . . . . . . . 19 $/\$
162	149, 151, 153, 151, 154, 156, 161	offveq 6558	. . . . . . . . . . . . . . . . . 18
163	147, 162	eqtrd 2461	. . . . . . . . . . . . . . . . 17
164	141, 163	syl5eq 2473	. . . . . . . . . . . . . . . 16
165	164	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
166	117, 165	eqtrd 2461	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167		nnm1nn0 10907	. . . . . . . . . . . . . . . . 17
168	1, 167	syl 17	. . . . . . . . . . . . . . . 16
169		0elfz 11883	. . . . . . . . . . . . . . . 16
170	168, 169	syl 17	. . . . . . . . . . . . . . 15
171	170	ad2antrr 730	. . . . . . . . . . . . . 14 $/\$ $/\$
172		fvex 5883	. . . . . . . . . . . . . . 15
173	172	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
174	108, 166, 171, 173	fvmptd 5962	. . . . . . . . . . . . 13 $/\$ $/\$
175	107, 174	sylan 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
176	175	an32s 811	. . . . . . . . . . 11 $/\$ $/\$ $/\$
177	103, 176	mpdan 672	. . . . . . . . . 10 $/\$ $/\$
178		fveq2 5873	. . . . . . . . . . . . . . . 16
179	178	eleq1d 2489	. . . . . . . . . . . . . . 15
180	179	anbi2d 708	. . . . . . . . . . . . . 14 $/\$ $/\$
181		fveq2 5873	. . . . . . . . . . . . . . . 16
182	181	fveq2d 5877	. . . . . . . . . . . . . . 15
183	182	eqeq2d 2434	. . . . . . . . . . . . . 14
184	180, 183	imbi12d 321	. . . . . . . . . . . . 13 $/\$ $/\$
185	174	expcom 436	. . . . . . . . . . . . 13 $/\$
186	184, 185	vtoclga 3142	. . . . . . . . . . . 12 $/\$
187	7, 186	mpcom 37	. . . . . . . . . . 11 $/\$
188	187	adantr 466	. . . . . . . . . 10 $/\$ $/\$
189	177, 188	eqtr3d 2463	. . . . . . . . 9 $/\$ $/\$
190	189	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
191	1	ad3antrrr 734	. . . . . . . . 9 $/\$ $/\$ $/\$
192	6	ad3antrrr 734	. . . . . . . . 9 $/\$ $/\$ $/\$
193		simpllr 767	. . . . . . . . 9 $/\$ $/\$ $/\$
194		simplr 760	. . . . . . . . 9 $/\$ $/\$ $/\$
195	35	adantr 466	. . . . . . . . . . . . . 14 $/\$ ..^
196		xpopth 6838	. . . . . . . . . . . . . 14 ..^ $/\$ ..^ $/\$
197	78, 195, 196	syl2anr 480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
198	33	adantr 466	. . . . . . . . . . . . . . 15 $/\$ ..^
199		xpopth 6838	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$
200	199	biimpd 210	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$
201	76, 198, 200	syl2anr 480	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
202	103, 201	mpan2d 678	. . . . . . . . . . . . 13 $/\$ $/\$
203	197, 202	sylbid 218	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
204	189, 203	mpand 679	. . . . . . . . . . 11 $/\$ $/\$
205	204	necon3d 2646	. . . . . . . . . 10 $/\$ $/\$
206	205	imp 430	. . . . . . . . 9 $/\$ $/\$ $/\$
207	191, 3, 192, 193, 194, 206	poimirlem9 31857	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
208	103	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
209	190, 207, 208	jca31 536	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
210	209	ex 435	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
211		simplr 760	. . . . . . . 8 $/\$ $\$ $/\$ $\$
212		elfznn 11822	. . . . . . . . . . . . . 14
213	212	nnred 10620	. . . . . . . . . . . . 13
214	213	ltp1d 10533	. . . . . . . . . . . . 13
215	213, 214	ltned 9767	. . . . . . . . . . . 12
216	215	adantl 467	. . . . . . . . . . 11 $/\$
217		fveq1 5872	. . . . . . . . . . . . 13 $\$ $\$
218		id 23	. . . . . . . . . . . . . . . . . . . . . 22
219		ltp1 10439	. . . . . . . . . . . . . . . . . . . . . 22
220	218, 219	ltned 9767	. . . . . . . . . . . . . . . . . . . . 21
221		fvex 5883	. . . . . . . . . . . . . . . . . . . . . 22
222		ovex 6325	. . . . . . . . . . . . . . . . . . . . . 22
223	221, 222, 222, 221	fpr 6079	. . . . . . . . . . . . . . . . . . . . 21
224	220, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20
225		f1oi 5858	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
226		f1of 5823	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$ $\$ $\$
227	225, 226	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
228		disjdif 3864	. . . . . . . . . . . . . . . . . . . . 21 $\$
229		fun 5755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
230	228, 229	mpan2 675	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
231	224, 227, 230	sylancl 666	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
232	221	prid1 4102	. . . . . . . . . . . . . . . . . . . 20
233		elun1 3630	. . . . . . . . . . . . . . . . . . . 20 $\$
234	232, 233	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
235		fvco3 5950	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $/\$ $\$ $\$ $\$
236	231, 234, 235	sylancl 666	. . . . . . . . . . . . . . . . . 18 $\$ $\$
237		ffn 5738	. . . . . . . . . . . . . . . . . . . . . 22
238	224, 237	syl 17	. . . . . . . . . . . . . . . . . . . . 21
239		fnresi 5703	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
240	228, 232	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
241		fvun1 5944	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$