poimirlem11 - Mathbox for Brendan Leahy

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

Theorem poimirlem11 31944

Description: Lemma for poimir 31966 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem12.2
poimirlem11.3
poimirlem11.4
poimirlem11.5
poimirlem11.6

**Assertion**
Ref	Expression
poimirlem11

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem11**
Step	Hyp	Ref	Expression
1		eldif 3413	. . . . . . 7 $\$ $/\$
2		imassrn 5178	. . . . . . . . . . . 12
3		poimirlem12.2	. . . . . . . . . . . . . . . . . 18
4		elrabi 3192	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
5		poimirlem22.s	. . . . . . . . . . . . . . . . . . 19 ..^
6	4, 5	eleq2s 2546	. . . . . . . . . . . . . . . . . 18 ..^
7	3, 6	syl 17	. . . . . . . . . . . . . . . . 17 ..^
8		xp1st 6820	. . . . . . . . . . . . . . . . 17 ..^ ..^
9	7, 8	syl 17	. . . . . . . . . . . . . . . 16 ..^
10		xp2nd 6821	. . . . . . . . . . . . . . . 16 ..^
11	9, 10	syl 17	. . . . . . . . . . . . . . 15
12		fvex 5873	. . . . . . . . . . . . . . . 16
13		f1oeq1 5803	. . . . . . . . . . . . . . . 16
14	12, 13	elab 3184	. . . . . . . . . . . . . . 15
15	11, 14	sylib 200	. . . . . . . . . . . . . 14
16		f1of 5812	. . . . . . . . . . . . . 14
17	15, 16	syl 17	. . . . . . . . . . . . 13
18		frn 5733	. . . . . . . . . . . . 13
19	17, 18	syl 17	. . . . . . . . . . . 12
20	2, 19	syl5ss 3442	. . . . . . . . . . 11
21		poimirlem11.4	. . . . . . . . . . . . . . . . 17
22		elrabi 3192	. . . . . . . . . . . . . . . . . 18 ..^ ..^
23	22, 5	eleq2s 2546	. . . . . . . . . . . . . . . . 17 ..^
24	21, 23	syl 17	. . . . . . . . . . . . . . . 16 ..^
25		xp1st 6820	. . . . . . . . . . . . . . . 16 ..^ ..^
26	24, 25	syl 17	. . . . . . . . . . . . . . 15 ..^
27		xp2nd 6821	. . . . . . . . . . . . . . 15 ..^
28	26, 27	syl 17	. . . . . . . . . . . . . 14
29		fvex 5873	. . . . . . . . . . . . . . 15
30		f1oeq1 5803	. . . . . . . . . . . . . . 15
31	29, 30	elab 3184	. . . . . . . . . . . . . 14
32	28, 31	sylib 200	. . . . . . . . . . . . 13
33		f1ofo 5819	. . . . . . . . . . . . 13
34	32, 33	syl 17	. . . . . . . . . . . 12
35		foima 5796	. . . . . . . . . . . 12
36	34, 35	syl 17	. . . . . . . . . . 11
37	20, 36	sseqtr4d 3468	. . . . . . . . . 10
38	37	ssdifd 3568	. . . . . . . . 9 $\$ $\$
39		dff1o3 5818	. . . . . . . . . . . . 13 $/\$
40	39	simprbi 466	. . . . . . . . . . . 12
41	32, 40	syl 17	. . . . . . . . . . 11
42		imadif 5656	. . . . . . . . . . 11 $\$ $\$
43	41, 42	syl 17	. . . . . . . . . 10 $\$ $\$
44		difun2 3846	. . . . . . . . . . . 12 $\$ $\$
45		poimirlem11.6	. . . . . . . . . . . . . . 15
46		fzsplit 11822	. . . . . . . . . . . . . . 15
47	45, 46	syl 17	. . . . . . . . . . . . . 14
48		uncom 3577	. . . . . . . . . . . . . 14
49	47, 48	syl6eq 2500	. . . . . . . . . . . . 13
50	49	difeq1d 3549	. . . . . . . . . . . 12 $\$ $\$
51		incom 3624	. . . . . . . . . . . . . 14
52		elfznn 11825	. . . . . . . . . . . . . . . . . 18
53	45, 52	syl 17	. . . . . . . . . . . . . . . . 17
54	53	nnred 10621	. . . . . . . . . . . . . . . 16
55	54	ltp1d 10534	. . . . . . . . . . . . . . 15
56		fzdisj 11823	. . . . . . . . . . . . . . 15
57	55, 56	syl 17	. . . . . . . . . . . . . 14
58	51, 57	syl5eq 2496	. . . . . . . . . . . . 13
59		disj3 3808	. . . . . . . . . . . . 13 $\$
60	58, 59	sylib 200	. . . . . . . . . . . 12 $\$
61	44, 50, 60	3eqtr4a 2510	. . . . . . . . . . 11 $\$
62	61	imaeq2d 5167	. . . . . . . . . 10 $\$
63	43, 62	eqtr3d 2486	. . . . . . . . 9 $\$
64	38, 63	sseqtrd 3467	. . . . . . . 8 $\$
65	64	sselda 3431	. . . . . . 7 $/\$ $\$
66	1, 65	sylan2br 479	. . . . . 6 $/\$ $/\$
67		fveq2 5863	. . . . . . . . . . . . . . . . . . 19
68	67	breq2d 4413	. . . . . . . . . . . . . . . . . 18
69	68	ifbid 3902	. . . . . . . . . . . . . . . . 17
70	69	csbeq1d 3369	. . . . . . . . . . . . . . . 16
71		fveq2 5863	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5867	. . . . . . . . . . . . . . . . . 18
73	71	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . 21
74	73	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . 20
75	74	xpeq1d 4856	. . . . . . . . . . . . . . . . . . 19
76	73	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . 20
77	76	xpeq1d 4856	. . . . . . . . . . . . . . . . . . 19
78	75, 77	uneq12d 3588	. . . . . . . . . . . . . . . . . 18
79	72, 78	oveq12d 6306	. . . . . . . . . . . . . . . . 17
80	79	csbeq2dv 3780	. . . . . . . . . . . . . . . 16
81	70, 80	eqtrd 2484	. . . . . . . . . . . . . . 15
82	81	mpteq2dv 4489	. . . . . . . . . . . . . 14
83	82	eqeq2d 2460	. . . . . . . . . . . . 13
84	83, 5	elrab2 3197	. . . . . . . . . . . 12 ..^ $/\$
85	84	simprbi 466	. . . . . . . . . . 11
86	21, 85	syl 17	. . . . . . . . . 10
87		poimirlem11.5	. . . . . . . . . . . . . . . 16
88		breq12 4406	. . . . . . . . . . . . . . . 16 $/\$
89	87, 88	sylan2 477	. . . . . . . . . . . . . . 15 $/\$
90	89	ancoms 455	. . . . . . . . . . . . . 14 $/\$
91		oveq1 6295	. . . . . . . . . . . . . . 15
92	53	nncnd 10622	. . . . . . . . . . . . . . . 16
93		npcan1 10041	. . . . . . . . . . . . . . . 16
94	92, 93	syl 17	. . . . . . . . . . . . . . 15
95	91, 94	sylan9eqr 2506	. . . . . . . . . . . . . 14 $/\$
96	90, 95	ifbieq2d 3905	. . . . . . . . . . . . 13 $/\$
97	53	nnzd 11036	. . . . . . . . . . . . . . . . . . 19
98		poimir.0	. . . . . . . . . . . . . . . . . . . 20
99	98	nnzd 11036	. . . . . . . . . . . . . . . . . . 19
100		elfzm1b 11869	. . . . . . . . . . . . . . . . . . 19 $/\$
101	97, 99, 100	syl2anc 666	. . . . . . . . . . . . . . . . . 18
102	45, 101	mpbid 214	. . . . . . . . . . . . . . . . 17
103		elfzle1 11799	. . . . . . . . . . . . . . . . 17
104	102, 103	syl 17	. . . . . . . . . . . . . . . 16
105		0red 9641	. . . . . . . . . . . . . . . . 17
106		nnm1nn0 10908	. . . . . . . . . . . . . . . . . . 19
107	53, 106	syl 17	. . . . . . . . . . . . . . . . . 18
108	107	nn0red 10923	. . . . . . . . . . . . . . . . 17
109	105, 108	lenltd 9778	. . . . . . . . . . . . . . . 16
110	104, 109	mpbid 214	. . . . . . . . . . . . . . 15
111	110	iffalsed 3891	. . . . . . . . . . . . . 14
112	111	adantr 467	. . . . . . . . . . . . 13 $/\$
113	96, 112	eqtrd 2484	. . . . . . . . . . . 12 $/\$
114	113	csbeq1d 3369	. . . . . . . . . . 11 $/\$
115		oveq2 6296	. . . . . . . . . . . . . . . . . 18
116	115	imaeq2d 5167	. . . . . . . . . . . . . . . . 17
117	116	xpeq1d 4856	. . . . . . . . . . . . . . . 16
118		oveq1 6295	. . . . . . . . . . . . . . . . . . 19
119	118	oveq1d 6303	. . . . . . . . . . . . . . . . . 18
120	119	imaeq2d 5167	. . . . . . . . . . . . . . . . 17
121	120	xpeq1d 4856	. . . . . . . . . . . . . . . 16
122	117, 121	uneq12d 3588	. . . . . . . . . . . . . . 15
123	122	oveq2d 6304	. . . . . . . . . . . . . 14
124	123	adantl 468	. . . . . . . . . . . . 13 $/\$
125	45, 124	csbied 3389	. . . . . . . . . . . 12
126	125	adantr 467	. . . . . . . . . . 11 $/\$
127	114, 126	eqtrd 2484	. . . . . . . . . 10 $/\$
128		ovex 6316	. . . . . . . . . . 11
129	128	a1i 11	. . . . . . . . . 10
130	86, 127, 102, 129	fvmptd 5952	. . . . . . . . 9
131	130	fveq1d 5865	. . . . . . . 8
132	131	adantr 467	. . . . . . 7 $/\$
133		imassrn 5178	. . . . . . . . . 10
134		f1of 5812	. . . . . . . . . . . 12
135	32, 134	syl 17	. . . . . . . . . . 11
136		frn 5733	. . . . . . . . . . 11
137	135, 136	syl 17	. . . . . . . . . 10
138	133, 137	syl5ss 3442	. . . . . . . . 9
139	138	sselda 3431	. . . . . . . 8 $/\$
140		xp1st 6820	. . . . . . . . . . . 12 ..^ ..^
141	26, 140	syl 17	. . . . . . . . . . 11 ..^
142		elmapfn 7491	. . . . . . . . . . 11 ..^
143	141, 142	syl 17	. . . . . . . . . 10
144	143	adantr 467	. . . . . . . . 9 $/\$
145		1ex 9635	. . . . . . . . . . . . . 14
146		fnconstg 5769	. . . . . . . . . . . . . 14
147	145, 146	ax-mp 5	. . . . . . . . . . . . 13
148		c0ex 9634	. . . . . . . . . . . . . 14
149		fnconstg 5769	. . . . . . . . . . . . . 14
150	148, 149	ax-mp 5	. . . . . . . . . . . . 13
151	147, 150	pm3.2i 457	. . . . . . . . . . . 12 $/\$
152		imain 5657	. . . . . . . . . . . . . 14
153	41, 152	syl 17	. . . . . . . . . . . . 13
154	57	imaeq2d 5167	. . . . . . . . . . . . . 14
155		ima0 5182	. . . . . . . . . . . . . 14
156	154, 155	syl6eq 2500	. . . . . . . . . . . . 13
157	153, 156	eqtr3d 2486	. . . . . . . . . . . 12
158		fnun 5680	. . . . . . . . . . . 12 $/\$ $/\$
159	151, 157, 158	sylancr 668	. . . . . . . . . . 11
160		imaundi 5247	. . . . . . . . . . . . 13
161	47	imaeq2d 5167	. . . . . . . . . . . . . 14
162	161, 36	eqtr3d 2486	. . . . . . . . . . . . 13
163	160, 162	syl5eqr 2498	. . . . . . . . . . . 12
164	163	fneq2d 5665	. . . . . . . . . . 11
165	159, 164	mpbid 214	. . . . . . . . . 10
166	165	adantr 467	. . . . . . . . 9 $/\$
167		ovex 6316	. . . . . . . . . 10
168	167	a1i 11	. . . . . . . . 9 $/\$
169		inidm 3640	. . . . . . . . 9
170		eqidd 2451	. . . . . . . . 9 $/\$ $/\$
171		fvun2 5935	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
172	147, 150, 171	mp3an12 1353	. . . . . . . . . . . 12 $/\$
173	157, 172	sylan 474	. . . . . . . . . . 11 $/\$
174	148	fvconst2 6118	. . . . . . . . . . . 12
175	174	adantl 468	. . . . . . . . . . 11 $/\$
176	173, 175	eqtrd 2484	. . . . . . . . . 10 $/\$
177	176	adantr 467	. . . . . . . . 9 $/\$ $/\$
178	144, 166, 168, 168, 169, 170, 177	ofval 6537	. . . . . . . 8 $/\$ $/\$
179	139, 178	mpdan 673	. . . . . . 7 $/\$
180		elmapi 7490	. . . . . . . . . . . . 13 ..^ ..^
181	141, 180	syl 17	. . . . . . . . . . . 12 ..^
182	181	ffvelrnda 6020	. . . . . . . . . . 11 $/\$ ..^
183		elfzonn0 11957	. . . . . . . . . . 11 ..^
184	182, 183	syl 17	. . . . . . . . . 10 $/\$
185	184	nn0cnd 10924	. . . . . . . . 9 $/\$
186	139, 185	syldan 473	. . . . . . . 8 $/\$
187	186	addid1d 9830	. . . . . . 7 $/\$
188	132, 179, 187	3eqtrd 2488	. . . . . 6 $/\$
189	66, 188	syldan 473	. . . . 5 $/\$ $/\$
190		fveq2 5863	. . . . . . . . . . . . . . . . . . 19
191	190	breq2d 4413	. . . . . . . . . . . . . . . . . 18
192	191	ifbid 3902	. . . . . . . . . . . . . . . . 17
193	192	csbeq1d 3369	. . . . . . . . . . . . . . . 16
194		fveq2 5863	. . . . . . . . . . . . . . . . . . 19
195	194	fveq2d 5867	. . . . . . . . . . . . . . . . . 18
196	194	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . 21
197	196	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . 20
198	197	xpeq1d 4856	. . . . . . . . . . . . . . . . . . 19
199	196	imaeq1d 5166	. . . . . . . . . . . . . . . . . . . 20
200	199	xpeq1d 4856	. . . . . . . . . . . . . . . . . . 19
201	198, 200	uneq12d 3588	. . . . . . . . . . . . . . . . . 18
202	195, 201	oveq12d 6306	. . . . . . . . . . . . . . . . 17
203	202	csbeq2dv 3780	. . . . . . . . . . . . . . . 16
204	193, 203	eqtrd 2484	. . . . . . . . . . . . . . 15
205	204	mpteq2dv 4489	. . . . . . . . . . . . . 14
206	205	eqeq2d 2460	. . . . . . . . . . . . 13
207	206, 5	elrab2 3197	. . . . . . . . . . . 12 ..^ $/\$
208	207	simprbi 466	. . . . . . . . . . 11
209	3, 208	syl 17	. . . . . . . . . 10
210		poimirlem11.3	. . . . . . . . . . . . . . . 16
211		breq12 4406	. . . . . . . . . . . . . . . 16 $/\$
212	210, 211	sylan2 477	. . . . . . . . . . . . . . 15 $/\$
213	212	ancoms 455	. . . . . . . . . . . . . 14 $/\$
214	213, 95	ifbieq2d 3905	. . . . . . . . . . . . 13 $/\$
215	214, 112	eqtrd 2484	. . . . . . . . . . . 12 $/\$
216	215	csbeq1d 3369	. . . . . . . . . . 11 $/\$
217	115	imaeq2d 5167	. . . . . . . . . . . . . . . . 17
218	217	xpeq1d 4856	. . . . . . . . . . . . . . . 16
219	119	imaeq2d 5167	. . . . . . . . . . . . . . . . 17
220	219	xpeq1d 4856	. . . . . . . . . . . . . . . 16
221	218, 220	uneq12d 3588	. . . . . . . . . . . . . . 15
222	221	oveq2d 6304	. . . . . . . . . . . . . 14
223	222	adantl 468	. . . . . . . . . . . . 13 $/\$
224	45, 223	csbied 3389	. . . . . . . . . . . 12
225	224	adantr 467	. . . . . . . . . . 11 $/\$
226	216, 225	eqtrd 2484	. . . . . . . . . 10 $/\$
227		ovex 6316	. . . . . . . . . . 11
228	227	a1i 11	. . . . . . . . . 10
229	209, 226, 102, 228	fvmptd 5952	. . . . . . . . 9
230	229	fveq1d 5865	. . . . . . . 8
231	230	adantr 467	. . . . . . 7 $/\$
232	20	sselda 3431	. . . . . . . 8 $/\$
233		xp1st 6820	. . . . . . . . . . . 12 ..^ ..^
234	9, 233	syl 17	. . . . . . . . . . 11 ..^
235		elmapfn 7491	. . . . . . . . . . 11 ..^
236	234, 235	syl 17	. . . . . . . . . 10
237	236	adantr 467	. . . . . . . . 9 $/\$
238		fnconstg 5769	. . . . . . . . . . . . . 14
239	145, 238	ax-mp 5	. . . . . . . . . . . . 13
240		fnconstg 5769	. . . . . . . . . . . . . 14
241	148, 240	ax-mp 5	. . . . . . . . . . . . 13
242	239, 241	pm3.2i 457	. . . . . . . . . . . 12 $/\$
243		dff1o3 5818	. . . . . . . . . . . . . . . 16 $/\$
244	243	simprbi 466	. . . . . . . . . . . . . . 15
245	15, 244	syl 17	. . . . . . . . . . . . . 14
246		imain 5657	. . . . . . . . . . . . . 14
247	245, 246	syl 17	. . . . . . . . . . . . 13
248	57	imaeq2d 5167	. . . . . . . . . . . . . 14
249		ima0 5182	. . . . . . . . . . . . . 14
250	248, 249	syl6eq 2500	. . . . . . . . . . . . 13
251	247, 250	eqtr3d 2486	. . . . . . . . . . . 12
252		fnun 5680	. . . . . . . . . . . 12 $/\$ $/\$
253	242, 251, 252	sylancr 668	. . . . . . . . . . 11
254		imaundi 5247	. . . . . . . . . . . . 13
255	47	imaeq2d 5167	. . . . . . . . . . . . . 14