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 32026

Description: Lemma for poimir 32037, 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 472	. . . 4 $/\$
3		poimirlem22.s	. . . 4 ..^
4		poimirlem22.1	. . . . 5
5	4	adantr 472	. . . 4 $/\$
6		poimirlem22.2	. . . . 5
7	6	adantr 472	. . . 4 $/\$
8		simpr 468	. . . 4 $/\$
9	2, 3, 5, 7, 8	poimirlem15 32019	. . 3 $/\$ $\$
10		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
11	10	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . 23
12	11	ifbid 3894	. . . . . . . . . . . . . . . . . . . . . 22
13	12	csbeq1d 3356	. . . . . . . . . . . . . . . . . . . . 21
14		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
15	14	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
16	14	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . 26
17	16	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . . . . . . 25
18	17	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . . . . 24
19	16	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . . . . 24
21	18, 20	uneq12d 3580	. . . . . . . . . . . . . . . . . . . . . . 23
22	15, 21	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . 22
23	22	csbeq2dv 3785	. . . . . . . . . . . . . . . . . . . . 21
24	13, 23	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20
25	24	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . 19
26	25	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18
27	26, 3	elrab2 3186	. . . . . . . . . . . . . . . . 17 ..^ $/\$
28	27	simprbi 471	. . . . . . . . . . . . . . . 16
29	6, 28	syl 17	. . . . . . . . . . . . . . 15
30	29	adantr 472	. . . . . . . . . . . . . 14 $/\$
31		elrabi 3181	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
32	31, 3	eleq2s 2567	. . . . . . . . . . . . . . . . . . . 20 ..^
33	6, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
34		xp1st 6842	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
36		xp1st 6842	. . . . . . . . . . . . . . . . . 18 ..^ ..^
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ..^
38		elmapi 7511	. . . . . . . . . . . . . . . . 17 ..^ ..^
39	37, 38	syl 17	. . . . . . . . . . . . . . . 16 ..^
40		elfzoelz 11947	. . . . . . . . . . . . . . . . 17 ..^
41	40	ssriv 3422	. . . . . . . . . . . . . . . 16 ..^
42		fss 5749	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
43	39, 41, 42	sylancl 675	. . . . . . . . . . . . . . 15
44	43	adantr 472	. . . . . . . . . . . . . 14 $/\$
45		xp2nd 6843	. . . . . . . . . . . . . . . . 17 ..^
46	35, 45	syl 17	. . . . . . . . . . . . . . . 16
47		fvex 5889	. . . . . . . . . . . . . . . . 17
48		f1oeq1 5818	. . . . . . . . . . . . . . . . 17
49	47, 48	elab 3173	. . . . . . . . . . . . . . . 16
50	46, 49	sylib 201	. . . . . . . . . . . . . . 15
51	50	adantr 472	. . . . . . . . . . . . . 14 $/\$
52	2, 30, 44, 51, 8	poimirlem1 32005	. . . . . . . . . . . . 13 $/\$
53	52	adantr 472	. . . . . . . . . . . 12 $/\$ $/\$
54	1	ad3antrrr 744	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
55		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . 23
57	56	ifbid 3894	. . . . . . . . . . . . . . . . . . . . . 22
58	57	csbeq1d 3356	. . . . . . . . . . . . . . . . . . . . 21
59		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . 24
60	59	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23
61	59	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	61	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	62	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . . . . 24
64	61	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . . . . . . 25
65	64	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . . . . 24
66	63, 65	uneq12d 3580	. . . . . . . . . . . . . . . . . . . . . . 23
67	60, 66	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . 22
68	67	csbeq2dv 3785	. . . . . . . . . . . . . . . . . . . . 21
69	58, 68	eqtrd 2505	. . . . . . . . . . . . . . . . . . . 20
70	69	mpteq2dv 4483	. . . . . . . . . . . . . . . . . . 19
71	70	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18
72	71, 3	elrab2 3186	. . . . . . . . . . . . . . . . 17 ..^ $/\$
73	72	simprbi 471	. . . . . . . . . . . . . . . 16
74	73	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
75		elrabi 3181	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
76	75, 3	eleq2s 2567	. . . . . . . . . . . . . . . . . . . 20 ..^
77		xp1st 6842	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
79		xp1st 6842	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
80	78, 79	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
81		elmapi 7511	. . . . . . . . . . . . . . . . . 18 ..^ ..^
82	80, 81	syl 17	. . . . . . . . . . . . . . . . 17 ..^
83		fss 5749	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^
84	82, 41, 83	sylancl 675	. . . . . . . . . . . . . . . 16
85	84	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
86		xp2nd 6843	. . . . . . . . . . . . . . . . . 18 ..^
87	78, 86	syl 17	. . . . . . . . . . . . . . . . 17
88		fvex 5889	. . . . . . . . . . . . . . . . . 18
89		f1oeq1 5818	. . . . . . . . . . . . . . . . . 18
90	88, 89	elab 3173	. . . . . . . . . . . . . . . . 17
91	87, 90	sylib 201	. . . . . . . . . . . . . . . 16
92	91	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
93		simpllr 777	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94		xp2nd 6843	. . . . . . . . . . . . . . . . . 18 ..^
95	76, 94	syl 17	. . . . . . . . . . . . . . . . 17
96	95	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
97		eldifsn 4088	. . . . . . . . . . . . . . . . 17 $\$ $/\$
98	97	biimpri 211	. . . . . . . . . . . . . . . 16 $/\$ $\$
99	96, 98	sylan 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
100	54, 74, 85, 92, 93, 99	poimirlem2 32006	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
101	100	ex 441	. . . . . . . . . . . . 13 $/\$ $/\$
102	101	necon1bd 2661	. . . . . . . . . . . 12 $/\$ $/\$
103	53, 102	mpd 15	. . . . . . . . . . 11 $/\$ $/\$
104		eleq1 2537	. . . . . . . . . . . . . . . 16
105	104	biimparc 495	. . . . . . . . . . . . . . 15 $/\$
106	105	anim2i 579	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
107	106	anassrs 660	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	73	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
109		breq1 4398	. . . . . . . . . . . . . . . . . 18
110		id 22	. . . . . . . . . . . . . . . . . 18
111	109, 110	ifbieq1d 3895	. . . . . . . . . . . . . . . . 17
112		elfznn 11854	. . . . . . . . . . . . . . . . . . . 20
113	112	nngt0d 10675	. . . . . . . . . . . . . . . . . . 19
114	113	iftrued 3880	. . . . . . . . . . . . . . . . . 18
115	114	ad2antlr 741	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	111, 115	sylan9eqr 2527	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
117	116	csbeq1d 3356	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
118		c0ex 9655	. . . . . . . . . . . . . . . . . 18
119		oveq2 6316	. . . . . . . . . . . . . . . . . . . . . . . 24
120		fz10 11846	. . . . . . . . . . . . . . . . . . . . . . . 24
121	119, 120	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . 23
122	121	imaeq2d 5174	. . . . . . . . . . . . . . . . . . . . . 22
123	122	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . 21
124		oveq1 6315	. . . . . . . . . . . . . . . . . . . . . . . . 25
125		0p1e1 10743	. . . . . . . . . . . . . . . . . . . . . . . . 25
126	124, 125	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . 24
127	126	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	imaeq2d 5174	. . . . . . . . . . . . . . . . . . . . . 22
129	128	xpeq1d 4862	. . . . . . . . . . . . . . . . . . . . 21
130	123, 129	uneq12d 3580	. . . . . . . . . . . . . . . . . . . 20
131		ima0 5189	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	xpeq1i 4859	. . . . . . . . . . . . . . . . . . . . . . 23
133		0xp 4920	. . . . . . . . . . . . . . . . . . . . . . 23
134	132, 133	eqtri 2493	. . . . . . . . . . . . . . . . . . . . . 22
135	134	uneq1i 3575	. . . . . . . . . . . . . . . . . . . . 21
136		uncom 3569	. . . . . . . . . . . . . . . . . . . . 21
137		un0 3762	. . . . . . . . . . . . . . . . . . . . 21
138	135, 136, 137	3eqtri 2497	. . . . . . . . . . . . . . . . . . . 20
139	130, 138	syl6eq 2521	. . . . . . . . . . . . . . . . . . 19
140	139	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
141	118, 140	csbie 3375	. . . . . . . . . . . . . . . . 17
142		f1ofo 5835	. . . . . . . . . . . . . . . . . . . . . 22
143	91, 142	syl 17	. . . . . . . . . . . . . . . . . . . . 21
144		foima 5811	. . . . . . . . . . . . . . . . . . . . 21
145	143, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20
146	145	xpeq1d 4862	. . . . . . . . . . . . . . . . . . 19
147	146	oveq2d 6324	. . . . . . . . . . . . . . . . . 18
148		ovex 6336	. . . . . . . . . . . . . . . . . . . 20
149	148	a1i 11	. . . . . . . . . . . . . . . . . . 19
150		ffn 5739	. . . . . . . . . . . . . . . . . . . 20 ..^
151	82, 150	syl 17	. . . . . . . . . . . . . . . . . . 19
152		fnconstg 5784	. . . . . . . . . . . . . . . . . . . 20
153	118, 152	mp1i 13	. . . . . . . . . . . . . . . . . . 19
154		eqidd 2472	. . . . . . . . . . . . . . . . . . 19 $/\$
155	118	fvconst2 6136	. . . . . . . . . . . . . . . . . . . 20
156	155	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
157	82	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
158		elfzonn0 11988	. . . . . . . . . . . . . . . . . . . . . 22 ..^
159	157, 158	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
160	159	nn0cnd 10951	. . . . . . . . . . . . . . . . . . . 20 $/\$
161	160	addid1d 9851	. . . . . . . . . . . . . . . . . . 19 $/\$
162	149, 151, 153, 151, 154, 156, 161	offveq 6571	. . . . . . . . . . . . . . . . . 18
163	147, 162	eqtrd 2505	. . . . . . . . . . . . . . . . 17
164	141, 163	syl5eq 2517	. . . . . . . . . . . . . . . 16
165	164	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
166	117, 165	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
167		nnm1nn0 10935	. . . . . . . . . . . . . . . . 17
168	1, 167	syl 17	. . . . . . . . . . . . . . . 16
169		0elfz 11915	. . . . . . . . . . . . . . . 16
170	168, 169	syl 17	. . . . . . . . . . . . . . 15
171	170	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$
172		fvex 5889	. . . . . . . . . . . . . . 15
173	172	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
174	108, 166, 171, 173	fvmptd 5969	. . . . . . . . . . . . 13 $/\$ $/\$
175	107, 174	sylan 479	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
176	175	an32s 821	. . . . . . . . . . 11 $/\$ $/\$ $/\$
177	103, 176	mpdan 681	. . . . . . . . . 10 $/\$ $/\$
178		fveq2 5879	. . . . . . . . . . . . . . . 16
179	178	eleq1d 2533	. . . . . . . . . . . . . . 15
180	179	anbi2d 718	. . . . . . . . . . . . . 14 $/\$ $/\$
181		fveq2 5879	. . . . . . . . . . . . . . . 16
182	181	fveq2d 5883	. . . . . . . . . . . . . . 15
183	182	eqeq2d 2481	. . . . . . . . . . . . . 14
184	180, 183	imbi12d 327	. . . . . . . . . . . . 13 $/\$ $/\$
185	174	expcom 442	. . . . . . . . . . . . 13 $/\$
186	184, 185	vtoclga 3099	. . . . . . . . . . . 12 $/\$
187	7, 186	mpcom 36	. . . . . . . . . . 11 $/\$
188	187	adantr 472	. . . . . . . . . 10 $/\$ $/\$
189	177, 188	eqtr3d 2507	. . . . . . . . 9 $/\$ $/\$
190	189	adantr 472	. . . . . . . 8 $/\$ $/\$ $/\$
191	1	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $/\$
192	6	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $/\$
193		simpllr 777	. . . . . . . . 9 $/\$ $/\$ $/\$
194		simplr 770	. . . . . . . . 9 $/\$ $/\$ $/\$
195	35	adantr 472	. . . . . . . . . . . . . 14 $/\$ ..^
196		xpopth 6851	. . . . . . . . . . . . . 14 ..^ $/\$ ..^ $/\$
197	78, 195, 196	syl2anr 486	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
198	33	adantr 472	. . . . . . . . . . . . . . 15 $/\$ ..^
199		xpopth 6851	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^ $/\$
200	199	biimpd 212	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ $/\$
201	76, 198, 200	syl2anr 486	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
202	103, 201	mpan2d 688	. . . . . . . . . . . . 13 $/\$ $/\$
203	197, 202	sylbid 223	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
204	189, 203	mpand 689	. . . . . . . . . . 11 $/\$ $/\$
205	204	necon3d 2664	. . . . . . . . . 10 $/\$ $/\$
206	205	imp 436	. . . . . . . . 9 $/\$ $/\$ $/\$
207	191, 3, 192, 193, 194, 206	poimirlem9 32013	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
208	103	adantr 472	. . . . . . . 8 $/\$ $/\$ $/\$
209	190, 207, 208	jca31 543	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
210	209	ex 441	. . . . . 6 $/\$ $/\$ $/\$ $\$ $/\$
211		simplr 770	. . . . . . . 8 $/\$ $\$ $/\$ $\$
212		elfznn 11854	. . . . . . . . . . . . . 14
213	212	nnred 10646	. . . . . . . . . . . . 13
214	213	ltp1d 10559	. . . . . . . . . . . . 13
215	213, 214	ltned 9788	. . . . . . . . . . . 12
216	215	adantl 473	. . . . . . . . . . 11 $/\$
217		fveq1 5878	. . . . . . . . . . . . 13 $\$ $\$
218		id 22	. . . . . . . . . . . . . . . . . . . . . 22
219		ltp1 10465	. . . . . . . . . . . . . . . . . . . . . 22
220	218, 219	ltned 9788	. . . . . . . . . . . . . . . . . . . . 21
221		fvex 5889	. . . . . . . . . . . . . . . . . . . . . 22
222		ovex 6336	. . . . . . . . . . . . . . . . . . . . . 22
223	221, 222, 222, 221	fpr 6088	. . . . . . . . . . . . . . . . . . . . 21
224	220, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20
225		f1oi 5864	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
226		f1of 5828	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$ $\$ $\$ $\$
227	225, 226	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
228		disjdif 3830	. . . . . . . . . . . . . . . . . . . . 21 $\$
229		fun 5758	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$ $\$ $/\$ $\$ $\$ $\$ $\$
230	228, 229	mpan2 685	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
231	224, 227, 230	sylancl 675	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
232	221	prid1 4071	. . . . . . . . . . . . . . . . . . . 20
233		elun1 3592	. . . . . . . . . . . . . . . . . . . 20 $\$
234	232, 233	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$
235		fvco3 5957	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $/\$ $\$ $\$ $\$
236	231, 234, 235	sylancl 675	. . . . . . . . . . . . . . . . . 18 $\$ $\$
237		ffn 5739	. . . . . . . . . . . . . . . . . . . . . 22
238	224, 237	syl 17	. . . . . . . . . . . . . . . . . . . . 21
239		fnresi 5703	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
240	228, 232	pm3.2i 462	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
241		fvun1 5951	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$