poimirlem22 - Mathbox for Brendan Leahy

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

Theorem poimirlem22 31955

Description: Lemma for poimir 31966, 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 467	. . . 4 $/\$
3		poimirlem22.s	. . . 4 ..^
4		poimirlem22.1	. . . . 5
5	4	adantr 467	. . . 4 $/\$
6		poimirlem22.2	. . . . 5
7	6	adantr 467	. . . 4 $/\$
8		simpr 463	. . . 4 $/\$
9	2, 3, 5, 7, 8	poimirlem15 31948	. . 3 $/\$ $\$
10		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . 24
11	10	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . 23
12	11	ifbid 3902	. . . . . . . . . . . . . . . . . . . . . 22
13	12	csbeq1d 3369	. . . . . . . . . . . . . . . . . . . . 21
14		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . 24
15	14	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . 23
16	14	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	16	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . . . . 24
19	16	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . . . . 24
21	18, 20	uneq12d 3588	. . . . . . . . . . . . . . . . . . . . . . 23
22	15, 21	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . . 22
23	22	csbeq2dv 3780	. . . . . . . . . . . . . . . . . . . . 21
24	13, 23	eqtrd 2484	. . . . . . . . . . . . . . . . . . . 20
25	24	mpteq2dv 4489	. . . . . . . . . . . . . . . . . . 19
26	25	eqeq2d 2460	. . . . . . . . . . . . . . . . . 18
27	26, 3	elrab2 3197	. . . . . . . . . . . . . . . . 17 ..^ $/\$
28	27	simprbi 466	. . . . . . . . . . . . . . . 16
29	6, 28	syl 17	. . . . . . . . . . . . . . 15
30	29	adantr 467	. . . . . . . . . . . . . 14 $/\$
31		elrabi 3192	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
32	31, 3	eleq2s 2546	. . . . . . . . . . . . . . . . . . . 20 ..^
33	6, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
34		xp1st 6820	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
36		xp1st 6820	. . . . . . . . . . . . . . . . . 18 ..^ ..^
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ..^
38		elmapi 7490	. . . . . . . . . . . . . . . . 17 ..^ ..^
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ..^
40		elfzoelz 11917	. . . . . . . . . . . . . . . . 17 ..^
41	40	ssriv 3435	. . . . . . . . . . . . . . . 16 ..^
42		fss 5735	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
43	39, 41, 42	sylancl 667	. . . . . . . . . . . . . . 15
44	43	adantr 467	. . . . . . . . . . . . . 14 $/\$
45		xp2nd 6821	. . . . . . . . . . . . . . . . 17 ..^
46	35, 45	syl 17	. . . . . . . . . . . . . . . 16
47		fvex 5873	. . . . . . . . . . . . . . . . 17
48		f1oeq1 5803	. . . . . . . . . . . . . . . . 17
49	47, 48	elab 3184	. . . . . . . . . . . . . . . 16
50	46, 49	sylib 200	. . . . . . . . . . . . . . 15
51	50	adantr 467	. . . . . . . . . . . . . 14 $/\$
52	2, 30, 44, 51, 8	poimirlem1 31934	. . . . . . . . . . . . 13 $/\$
53	52	adantr 467	. . . . . . . . . . . 12 $/\$ $/\$
54	1	ad3antrrr 735	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
55		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . 23
57	56	ifbid 3902	. . . . . . . . . . . . . . . . . . . . . 22
58	57	csbeq1d 3369	. . . . . . . . . . . . . . . . . . . . 21
59		fveq2 5863	. . . . . . . . . . . . . . . . . . . . . . . 24
60	59	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . 23
61	59	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	61	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	62	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . . . . 24
64	61	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	64	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . . . . 24
66	63, 65	uneq12d 3588	. . . . . . . . . . . . . . . . . . . . . . 23
67	60, 66	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . . 22
68	67	csbeq2dv 3780	. . . . . . . . . . . . . . . . . . . . 21
69	58, 68	eqtrd 2484	. . . . . . . . . . . . . . . . . . . 20
70	69	mpteq2dv 4489	. . . . . . . . . . . . . . . . . . 19
71	70	eqeq2d 2460	. . . . . . . . . . . . . . . . . 18
72	71, 3	elrab2 3197	. . . . . . . . . . . . . . . . 17 ..^ $/\$
73	72	simprbi 466	. . . . . . . . . . . . . . . 16
74	73	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		elrabi 3192	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
76	75, 3	eleq2s 2546	. . . . . . . . . . . . . . . . . . . 20 ..^
77		xp1st 6820	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
79		xp1st 6820	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
81		elmapi 7490	. . . . . . . . . . . . . . . . . 18 ..^ ..^
82	80, 81	syl 17	. . . . . . . . . . . . . . . . 17 ..^
83		fss 5735	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
84	82, 41, 83	sylancl 667	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86		xp2nd 6821	. . . . . . . . . . . . . . . . . 18 ..^
87	78, 86	syl 17	. . . . . . . . . . . . . . . . 17
88		fvex 5873	. . . . . . . . . . . . . . . . . 18
89		f1oeq1 5803	. . . . . . . . . . . . . . . . . 18
90	88, 89	elab 3184	. . . . . . . . . . . . . . . . 17
91	87, 90	sylib 200	. . . . . . . . . . . . . . . 16
92	91	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93		simpllr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94		xp2nd 6821	. . . . . . . . . . . . . . . . . 18 ..^
95	76, 94	syl 17	. . . . . . . . . . . . . . . . 17
96	95	adantl 468	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97		eldifsn 4096	. . . . . . . . . . . . . . . . 17 $\$ $/\$
98	97	biimpri 210	. . . . . . . . . . . . . . . 16 $/\$ $\$
99	96, 98	sylan 474	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
100	54, 74, 85, 92, 93, 99	poimirlem2 31935	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100	ex 436	. . . . . . . . . . . . 13 $/\$ $/\$
102	101	necon1bd 2641	. . . . . . . . . . . 12 $/\$ $/\$
103	53, 102	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
104		eleq1 2516	. . . . . . . . . . . . . . . 16
105	104	biimparc 490	. . . . . . . . . . . . . . 15 $/\$
106	105	anim2i 572	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	106	anassrs 653	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	73	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
109		breq1 4404	. . . . . . . . . . . . . . . . . 18
110		id 22	. . . . . . . . . . . . . . . . . 18
111	109, 110	ifbieq1d 3903	. . . . . . . . . . . . . . . . 17
112		elfznn 11825	. . . . . . . . . . . . . . . . . . . 20
113	112	nngt0d 10650	. . . . . . . . . . . . . . . . . . 19
114	113	iftrued 3888	. . . . . . . . . . . . . . . . . 18
115	114	ad2antlr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	111, 115	sylan9eqr 2506	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117	116	csbeq1d 3369	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
118		c0ex 9634	. . . . . . . . . . . . . . . . . 18
119		oveq2 6296	. . . . . . . . . . . . . . . . . . . . . . . 24
120		fz10 11817	. . . . . . . . . . . . . . . . . . . . . . . 24
121	119, 120	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	imaeq2d 5167	. . . . . . . . . . . . . . . . . . . . . 22
123	122	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . 21
124		oveq1 6295	. . . . . . . . . . . . . . . . . . . . . . . . 25
125		0p1e1 10718	. . . . . . . . . . . . . . . . . . . . . . . . 25
126	124, 125	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . 24
127	126	oveq1d 6303	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	imaeq2d 5167	. . . . . . . . . . . . . . . . . . . . . 22
129	128	xpeq1d 4856	. . . . . . . . . . . . . . . . . . . . 21
130	123, 129	uneq12d 3588	. . . . . . . . . . . . . . . . . . . 20
131		ima0 5182	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	xpeq1i 4853	. . . . . . . . . . . . . . . . . . . . . . 23
133		0xp 4914	. . . . . . . . . . . . . . . . . . . . . . 23
134	132, 133	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . 22
135	134	uneq1i 3583	. . . . . . . . . . . . . . . . . . . . 21
136		uncom 3577	. . . . . . . . . . . . . . . . . . . . 21
137		un0 3758	. . . . . . . . . . . . . . . . . . . . 21
138	135, 136, 137	3eqtri 2476	. . . . . . . . . . . . . . . . . . . 20
139	130, 138	syl6eq 2500	. . . . . . . . . . . . . . . . . . 19
140	139	oveq2d 6304	. . . . . . . . . . . . . . . . . 18
141	118, 140	csbie 3388	. . . . . . . . . . . . . . . . 17
142		f1ofo 5819	. . . . . . . . . . . . . . . . . . . . . 22
143	91, 142	syl 17	. . . . . . . . . . . . . . . . . . . . 21
144		foima 5796	. . . . . . . . . . . . . . . . . . . . 21
145	143, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20
146	145	xpeq1d 4856	. . . . . . . . . . . . . . . . . . 19
147	146	oveq2d 6304	. . . . . . . . . . . . . . . . . 18
148		ovex 6316	. . . . . . . . . . . . . . . . . . . 20
149	148	a1i 11	. . . . . . . . . . . . . . . . . . 19
150		ffn 5726	. . . . . . . . . . . . . . . . . . . 20 ..^
151	82, 150	syl 17	. . . . . . . . . . . . . . . . . . 19
152		fnconstg 5769	. . . . . . . . . . . . . . . . . . . 20
153	118, 152	mp1i 13	. . . . . . . . . . . . . . . . . . 19
154		eqidd 2451	. . . . . . . . . . . . . . . . . . 19 $/\$
155	118	fvconst2 6118	. . . . . . . . . . . . . . . . . . . 20
156	155	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
157	82	ffvelrnda 6020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
158		elfzonn0 11957	. . . . . . . . . . . . . . . . . . . . . 22 ..^
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
160	159	nn0cnd 10924	. . . . . . . . . . . . . . . . . . . 20 $/\$
161	160	addid1d 9830	. . . . . . . . . . . . . . . . . . 19 $/\$
162	149, 151, 153, 151, 154, 156, 161	offveq 6549	. . . . . . . . . . . . . . . . . 18
163	147, 162	eqtrd 2484	. . . . . . . . . . . . . . . . 17
164	141, 163	syl5eq 2496	. . . . . . . . . . . . . . . 16
165	164	ad2antlr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
166	117, 165	eqtrd 2484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167		nnm1nn0 10908	. . . . . . . . . . . . . . . . 17
168	1, 167	syl 17	. . . . . . . . . . . . . . . 16
169		0elfz 11886	. . . . . . . . . . . . . . . 16
170	168, 169	syl 17	. . . . . . . . . . . . . . 15
171	170	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $/\$
172		fvex 5873	. . . . . . . . . . . . . . 15
173	172	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
174	108, 166, 171, 173	fvmptd 5952	. . . . . . . . . . . . 13 $/\$ $/\$
175	107, 174	sylan 474	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
176	175	an32s 812	. . . . . . . . . . 11 $/\$ $/\$ $/\$
177	103, 176	mpdan 673	. . . . . . . . . 10 $/\$ $/\$
178		fveq2 5863	. . . . . . . . . . . . . . . 16
179	178	eleq1d 2512	. . . . . . . . . . . . . . 15
180	179	anbi2d 709	. . . . . . . . . . . . . 14 $/\$ $/\$
181		fveq2 5863	. . . . . . . . . . . . . . . 16
182	181	fveq2d 5867	. . . . . . . . . . . . . . 15
183	182	eqeq2d 2460	. . . . . . . . . . . . . 14
184	180, 183	imbi12d 322	. . . . . . . . . . . . 13 $/\$ $/\$
185	174	expcom 437	. . . . . . . . . . . . 13 $/\$
186	184, 185	vtoclga 3112	. . . . . . . . . . . 12 $/\$
187	7, 186	mpcom 37	. . . . . . . . . . 11 $/\$
188	187	adantr 467	. . . . . . . . . 10 $/\$ $/\$
189	177, 188	eqtr3d 2486	. . . . . . . . 9 $/\$ $/\$
190	189	adantr 467	. . . . . . . 8 $/\$ $/\$ $/\$
191	1	ad3antrrr 735	. . . . . . . . 9 $/\$ $/\$ $/\$
192	6	ad3antrrr 735	. . . . . . . . 9 $/\$ $/\$ $/\$
193		simpllr 768	. . . . . . . . 9 $/\$ $/\$ $/\$
194		simplr 761	. . . . . . . . 9 $/\$ $/\$ $/\$
195	35	adantr 467	. . . . . . . . . . . . . 14 $/\$ ..^
196		xpopth 6829	. . . . . . . . . . . . . 14 ..^ $/\$ ..^ $/\$
197	78, 195, 196	syl2anr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
198	33	adantr 467	. . . . . . . . . . . . . . 15 $/\$ ..^
199		xpopth 6829	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$
200	199	biimpd 211	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$
201	76, 198, 200	syl2anr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
202	103, 201	mpan2d 679	. . . . . . . . . . . . 13 $/\$ $/\$
203	197, 202	sylbid 219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
204	189, 203	mpand 680	. . . . . . . . . . 11 $/\$ $/\$
205	204	necon3d 2644	. . . . . . . . . 10 $/\$ $/\$
206	205	imp 431	. . . . . . . . 9 $/\$ $/\$ $/\$
207	191, 3, 192, 193, 194, 206	poimirlem9 31942	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
208	103	adantr 467	. . . . . . . 8 $/\$ $/\$ $/\$
209	190, 207, 208	jca31 537	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
210	209	ex 436	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
211		simplr 761	. . . . . . . 8 $/\$ $\$ $/\$ $\$
212		elfznn 11825	. . . . . . . . . . . . . 14
213	212	nnred 10621	. . . . . . . . . . . . 13
214	213	ltp1d 10534	. . . . . . . . . . . . 13
215	213, 214	ltned 9768	. . . . . . . . . . . 12
216	215	adantl 468	. . . . . . . . . . 11 $/\$
217		fveq1 5862	. . . . . . . . . . . . 13 $\$ $\$
218		id 22	. . . . . . . . . . . . . . . . . . . . . 22
219		ltp1 10440	. . . . . . . . . . . . . . . . . . . . . 22
220	218, 219	ltned 9768	. . . . . . . . . . . . . . . . . . . . 21
221		fvex 5873	. . . . . . . . . . . . . . . . . . . . . 22
222		ovex 6316	. . . . . . . . . . . . . . . . . . . . . 22
223	221, 222, 222, 221	fpr 6070	. . . . . . . . . . . . . . . . . . . . 21
224	220, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20
225		f1oi 5848	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
226		f1of 5812	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$ $\$ $\$
227	225, 226	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
228		disjdif 3838	. . . . . . . . . . . . . . . . . . . . 21 $\$
229		fun 5744	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
230	228, 229	mpan2 676	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
231	224, 227, 230	sylancl 667	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
232	221	prid1 4079	. . . . . . . . . . . . . . . . . . . 20
233		elun1 3600	. . . . . . . . . . . . . . . . . . . 20 $\$
234	232, 233	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
235		fvco3 5940	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $/\$ $\$ $\$ $\$
236	231, 234, 235	sylancl 667	. . . . . . . . . . . . . . . . . 18 $\$ $\$
237		ffn 5726	. . . . . . . . . . . . . . . . . . . . . 22
238	224, 237	syl 17	. . . . . . . . . . . . . . . . . . . . 21
239		fnresi 5691	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
240	228, 232	pm3.2i 457	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
241		fvun1 5934	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$