poimirlem11 - Mathbox for Brendan Leahy

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

Theorem poimirlem11 31871

Description: Lemma for poimir 31893 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 3447	. . . . . . 7 $\$ $/\$
2		imassrn 5196	. . . . . . . . . . . 12
3		poimirlem12.2	. . . . . . . . . . . . . . . . . 18
4		elrabi 3227	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
5		poimirlem22.s	. . . . . . . . . . . . . . . . . . 19 ..^
6	4, 5	eleq2s 2531	. . . . . . . . . . . . . . . . . 18 ..^
7	3, 6	syl 17	. . . . . . . . . . . . . . . . 17 ..^
8		xp1st 6835	. . . . . . . . . . . . . . . . 17 ..^ ..^
9	7, 8	syl 17	. . . . . . . . . . . . . . . 16 ..^
10		xp2nd 6836	. . . . . . . . . . . . . . . 16 ..^
11	9, 10	syl 17	. . . . . . . . . . . . . . 15
12		fvex 5889	. . . . . . . . . . . . . . . 16
13		f1oeq1 5820	. . . . . . . . . . . . . . . 16
14	12, 13	elab 3219	. . . . . . . . . . . . . . 15
15	11, 14	sylib 200	. . . . . . . . . . . . . 14
16		f1of 5829	. . . . . . . . . . . . . 14
17	15, 16	syl 17	. . . . . . . . . . . . 13
18		frn 5750	. . . . . . . . . . . . 13
19	17, 18	syl 17	. . . . . . . . . . . 12
20	2, 19	syl5ss 3476	. . . . . . . . . . 11
21		poimirlem11.4	. . . . . . . . . . . . . . . . 17
22		elrabi 3227	. . . . . . . . . . . . . . . . . 18 ..^ ..^
23	22, 5	eleq2s 2531	. . . . . . . . . . . . . . . . 17 ..^
24	21, 23	syl 17	. . . . . . . . . . . . . . . 16 ..^
25		xp1st 6835	. . . . . . . . . . . . . . . 16 ..^ ..^
26	24, 25	syl 17	. . . . . . . . . . . . . . 15 ..^
27		xp2nd 6836	. . . . . . . . . . . . . . 15 ..^
28	26, 27	syl 17	. . . . . . . . . . . . . 14
29		fvex 5889	. . . . . . . . . . . . . . 15
30		f1oeq1 5820	. . . . . . . . . . . . . . 15
31	29, 30	elab 3219	. . . . . . . . . . . . . 14
32	28, 31	sylib 200	. . . . . . . . . . . . 13
33		f1ofo 5836	. . . . . . . . . . . . 13
34	32, 33	syl 17	. . . . . . . . . . . 12
35		foima 5813	. . . . . . . . . . . 12
36	34, 35	syl 17	. . . . . . . . . . 11
37	20, 36	sseqtr4d 3502	. . . . . . . . . 10
38	37	ssdifd 3602	. . . . . . . . 9 $\$ $\$
39		dff1o3 5835	. . . . . . . . . . . . 13 $/\$
40	39	simprbi 466	. . . . . . . . . . . 12
41	32, 40	syl 17	. . . . . . . . . . 11
42		imadif 5674	. . . . . . . . . . 11 $\$ $\$
43	41, 42	syl 17	. . . . . . . . . 10 $\$ $\$
44		difun2 3876	. . . . . . . . . . . 12 $\$ $\$
45		poimirlem11.6	. . . . . . . . . . . . . . 15
46		fzsplit 11827	. . . . . . . . . . . . . . 15
47	45, 46	syl 17	. . . . . . . . . . . . . 14
48		uncom 3611	. . . . . . . . . . . . . 14
49	47, 48	syl6eq 2480	. . . . . . . . . . . . 13
50	49	difeq1d 3583	. . . . . . . . . . . 12 $\$ $\$
51		incom 3656	. . . . . . . . . . . . . 14
52		elfznn 11830	. . . . . . . . . . . . . . . . . 18
53	45, 52	syl 17	. . . . . . . . . . . . . . . . 17
54	53	nnred 10626	. . . . . . . . . . . . . . . 16
55	54	ltp1d 10539	. . . . . . . . . . . . . . 15
56		fzdisj 11828	. . . . . . . . . . . . . . 15
57	55, 56	syl 17	. . . . . . . . . . . . . 14
58	51, 57	syl5eq 2476	. . . . . . . . . . . . 13
59		disj3 3838	. . . . . . . . . . . . 13 $\$
60	58, 59	sylib 200	. . . . . . . . . . . 12 $\$
61	44, 50, 60	3eqtr4a 2490	. . . . . . . . . . 11 $\$
62	61	imaeq2d 5185	. . . . . . . . . 10 $\$
63	43, 62	eqtr3d 2466	. . . . . . . . 9 $\$
64	38, 63	sseqtrd 3501	. . . . . . . 8 $\$
65	64	sselda 3465	. . . . . . 7 $/\$ $\$
66	1, 65	sylan2br 479	. . . . . 6 $/\$ $/\$
67		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
68	67	breq2d 4433	. . . . . . . . . . . . . . . . . 18
69	68	ifbid 3932	. . . . . . . . . . . . . . . . 17
70	69	csbeq1d 3403	. . . . . . . . . . . . . . . 16
71		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
72	71	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
73	71	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
74	73	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
75	74	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
76	73	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
77	76	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
78	75, 77	uneq12d 3622	. . . . . . . . . . . . . . . . . 18
79	72, 78	oveq12d 6321	. . . . . . . . . . . . . . . . 17
80	79	csbeq2dv 3810	. . . . . . . . . . . . . . . 16
81	70, 80	eqtrd 2464	. . . . . . . . . . . . . . 15
82	81	mpteq2dv 4509	. . . . . . . . . . . . . 14
83	82	eqeq2d 2437	. . . . . . . . . . . . 13
84	83, 5	elrab2 3232	. . . . . . . . . . . 12 ..^ $/\$
85	84	simprbi 466	. . . . . . . . . . 11
86	21, 85	syl 17	. . . . . . . . . 10
87		poimirlem11.5	. . . . . . . . . . . . . . . 16
88		breq12 4426	. . . . . . . . . . . . . . . 16 $/\$
89	87, 88	sylan2 477	. . . . . . . . . . . . . . 15 $/\$
90	89	ancoms 455	. . . . . . . . . . . . . 14 $/\$
91		oveq1 6310	. . . . . . . . . . . . . . 15
92	53	nncnd 10627	. . . . . . . . . . . . . . . 16
93		npcan1 10046	. . . . . . . . . . . . . . . 16
94	92, 93	syl 17	. . . . . . . . . . . . . . 15
95	91, 94	sylan9eqr 2486	. . . . . . . . . . . . . 14 $/\$
96	90, 95	ifbieq2d 3935	. . . . . . . . . . . . 13 $/\$
97	53	nnzd 11041	. . . . . . . . . . . . . . . . . . 19
98		poimir.0	. . . . . . . . . . . . . . . . . . . 20
99	98	nnzd 11041	. . . . . . . . . . . . . . . . . . 19
100		elfzm1b 11874	. . . . . . . . . . . . . . . . . . 19 $/\$
101	97, 99, 100	syl2anc 666	. . . . . . . . . . . . . . . . . 18
102	45, 101	mpbid 214	. . . . . . . . . . . . . . . . 17
103		elfzle1 11804	. . . . . . . . . . . . . . . . 17
104	102, 103	syl 17	. . . . . . . . . . . . . . . 16
105		0red 9646	. . . . . . . . . . . . . . . . 17
106		nnm1nn0 10913	. . . . . . . . . . . . . . . . . . 19
107	53, 106	syl 17	. . . . . . . . . . . . . . . . . 18
108	107	nn0red 10928	. . . . . . . . . . . . . . . . 17
109	105, 108	lenltd 9783	. . . . . . . . . . . . . . . 16
110	104, 109	mpbid 214	. . . . . . . . . . . . . . 15
111	110	iffalsed 3921	. . . . . . . . . . . . . 14
112	111	adantr 467	. . . . . . . . . . . . 13 $/\$
113	96, 112	eqtrd 2464	. . . . . . . . . . . 12 $/\$
114	113	csbeq1d 3403	. . . . . . . . . . 11 $/\$
115		oveq2 6311	. . . . . . . . . . . . . . . . . 18
116	115	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
117	116	xpeq1d 4874	. . . . . . . . . . . . . . . 16
118		oveq1 6310	. . . . . . . . . . . . . . . . . . 19
119	118	oveq1d 6318	. . . . . . . . . . . . . . . . . 18
120	119	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
121	120	xpeq1d 4874	. . . . . . . . . . . . . . . 16
122	117, 121	uneq12d 3622	. . . . . . . . . . . . . . 15
123	122	oveq2d 6319	. . . . . . . . . . . . . 14
124	123	adantl 468	. . . . . . . . . . . . 13 $/\$
125	45, 124	csbied 3423	. . . . . . . . . . . 12
126	125	adantr 467	. . . . . . . . . . 11 $/\$
127	114, 126	eqtrd 2464	. . . . . . . . . 10 $/\$
128		ovex 6331	. . . . . . . . . . 11
129	128	a1i 11	. . . . . . . . . 10
130	86, 127, 102, 129	fvmptd 5968	. . . . . . . . 9
131	130	fveq1d 5881	. . . . . . . 8
132	131	adantr 467	. . . . . . 7 $/\$
133		imassrn 5196	. . . . . . . . . 10
134		f1of 5829	. . . . . . . . . . . 12
135	32, 134	syl 17	. . . . . . . . . . 11
136		frn 5750	. . . . . . . . . . 11
137	135, 136	syl 17	. . . . . . . . . 10
138	133, 137	syl5ss 3476	. . . . . . . . 9
139	138	sselda 3465	. . . . . . . 8 $/\$
140		xp1st 6835	. . . . . . . . . . . 12 ..^ ..^
141	26, 140	syl 17	. . . . . . . . . . 11 ..^
142		elmapfn 7500	. . . . . . . . . . 11 ..^
143	141, 142	syl 17	. . . . . . . . . 10
144	143	adantr 467	. . . . . . . . 9 $/\$
145		1ex 9640	. . . . . . . . . . . . . 14
146		fnconstg 5786	. . . . . . . . . . . . . 14
147	145, 146	ax-mp 5	. . . . . . . . . . . . 13
148		c0ex 9639	. . . . . . . . . . . . . 14
149		fnconstg 5786	. . . . . . . . . . . . . 14
150	148, 149	ax-mp 5	. . . . . . . . . . . . 13
151	147, 150	pm3.2i 457	. . . . . . . . . . . 12 $/\$
152		imain 5675	. . . . . . . . . . . . . 14
153	41, 152	syl 17	. . . . . . . . . . . . 13
154	57	imaeq2d 5185	. . . . . . . . . . . . . 14
155		ima0 5200	. . . . . . . . . . . . . 14
156	154, 155	syl6eq 2480	. . . . . . . . . . . . 13
157	153, 156	eqtr3d 2466	. . . . . . . . . . . 12
158		fnun 5698	. . . . . . . . . . . 12 $/\$ $/\$
159	151, 157, 158	sylancr 668	. . . . . . . . . . 11
160		imaundi 5265	. . . . . . . . . . . . 13
161	47	imaeq2d 5185	. . . . . . . . . . . . . 14
162	161, 36	eqtr3d 2466	. . . . . . . . . . . . 13
163	160, 162	syl5eqr 2478	. . . . . . . . . . . 12
164	163	fneq2d 5683	. . . . . . . . . . 11
165	159, 164	mpbid 214	. . . . . . . . . 10
166	165	adantr 467	. . . . . . . . 9 $/\$
167		ovex 6331	. . . . . . . . . 10
168	167	a1i 11	. . . . . . . . 9 $/\$
169		inidm 3672	. . . . . . . . 9
170		eqidd 2424	. . . . . . . . 9 $/\$ $/\$
171		fvun2 5951	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
172	147, 150, 171	mp3an12 1351	. . . . . . . . . . . 12 $/\$
173	157, 172	sylan 474	. . . . . . . . . . 11 $/\$
174	148	fvconst2 6133	. . . . . . . . . . . 12
175	174	adantl 468	. . . . . . . . . . 11 $/\$
176	173, 175	eqtrd 2464	. . . . . . . . . 10 $/\$
177	176	adantr 467	. . . . . . . . 9 $/\$ $/\$
178	144, 166, 168, 168, 169, 170, 177	ofval 6552	. . . . . . . 8 $/\$ $/\$
179	139, 178	mpdan 673	. . . . . . 7 $/\$
180		elmapi 7499	. . . . . . . . . . . . 13 ..^ ..^
181	141, 180	syl 17	. . . . . . . . . . . 12 ..^
182	181	ffvelrnda 6035	. . . . . . . . . . 11 $/\$ ..^
183		elfzonn0 11962	. . . . . . . . . . 11 ..^
184	182, 183	syl 17	. . . . . . . . . 10 $/\$
185	184	nn0cnd 10929	. . . . . . . . 9 $/\$
186	139, 185	syldan 473	. . . . . . . 8 $/\$
187	186	addid1d 9835	. . . . . . 7 $/\$
188	132, 179, 187	3eqtrd 2468	. . . . . 6 $/\$
189	66, 188	syldan 473	. . . . 5 $/\$ $/\$
190		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
191	190	breq2d 4433	. . . . . . . . . . . . . . . . . 18
192	191	ifbid 3932	. . . . . . . . . . . . . . . . 17
193	192	csbeq1d 3403	. . . . . . . . . . . . . . . 16
194		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
195	194	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
196	194	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
197	196	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
198	197	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
199	196	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
200	199	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
201	198, 200	uneq12d 3622	. . . . . . . . . . . . . . . . . 18
202	195, 201	oveq12d 6321	. . . . . . . . . . . . . . . . 17
203	202	csbeq2dv 3810	. . . . . . . . . . . . . . . 16
204	193, 203	eqtrd 2464	. . . . . . . . . . . . . . 15
205	204	mpteq2dv 4509	. . . . . . . . . . . . . 14
206	205	eqeq2d 2437	. . . . . . . . . . . . 13
207	206, 5	elrab2 3232	. . . . . . . . . . . 12 ..^ $/\$
208	207	simprbi 466	. . . . . . . . . . 11
209	3, 208	syl 17	. . . . . . . . . 10
210		poimirlem11.3	. . . . . . . . . . . . . . . 16
211		breq12 4426	. . . . . . . . . . . . . . . 16 $/\$
212	210, 211	sylan2 477	. . . . . . . . . . . . . . 15 $/\$
213	212	ancoms 455	. . . . . . . . . . . . . 14 $/\$
214	213, 95	ifbieq2d 3935	. . . . . . . . . . . . 13 $/\$
215	214, 112	eqtrd 2464	. . . . . . . . . . . 12 $/\$
216	215	csbeq1d 3403	. . . . . . . . . . 11 $/\$
217	115	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
218	217	xpeq1d 4874	. . . . . . . . . . . . . . . 16
219	119	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
220	219	xpeq1d 4874	. . . . . . . . . . . . . . . 16
221	218, 220	uneq12d 3622	. . . . . . . . . . . . . . 15
222	221	oveq2d 6319	. . . . . . . . . . . . . 14
223	222	adantl 468	. . . . . . . . . . . . 13 $/\$
224	45, 223	csbied 3423	. . . . . . . . . . . 12
225	224	adantr 467	. . . . . . . . . . 11 $/\$
226	216, 225	eqtrd 2464	. . . . . . . . . 10 $/\$
227		ovex 6331	. . . . . . . . . . 11
228	227	a1i 11	. . . . . . . . . 10
229	209, 226, 102, 228	fvmptd 5968	. . . . . . . . 9
230	229	fveq1d 5881	. . . . . . . 8
231	230	adantr 467	. . . . . . 7 $/\$
232	20	sselda 3465	. . . . . . . 8 $/\$
233		xp1st 6835	. . . . . . . . . . . 12 ..^ ..^
234	9, 233	syl 17	. . . . . . . . . . 11 ..^
235		elmapfn 7500	. . . . . . . . . . 11 ..^
236	234, 235	syl 17	. . . . . . . . . 10
237	236	adantr 467	. . . . . . . . 9 $/\$
238		fnconstg 5786	. . . . . . . . . . . . . 14
239	145, 238	ax-mp 5	. . . . . . . . . . . . 13
240		fnconstg 5786	. . . . . . . . . . . . . 14
241	148, 240	ax-mp 5	. . . . . . . . . . . . 13
242	239, 241	pm3.2i 457	. . . . . . . . . . . 12 $/\$
243		dff1o3 5835	. . . . . . . . . . . . . . . 16 $/\$
244	243	simprbi 466	. . . . . . . . . . . . . . 15
245	15, 244	syl 17	. . . . . . . . . . . . . 14
246		imain 5675	. . . . . . . . . . . . . 14
247	245, 246	syl 17	. . . . . . . . . . . . 13
248	57	imaeq2d 5185	. . . . . . . . . . . . . 14
249		ima0 5200	. . . . . . . . . . . . . 14
250	248, 249	syl6eq 2480	. . . . . . . . . . . . 13
251	247, 250	eqtr3d 2466	. . . . . . . . . . . 12
252		fnun 5698	. . . . . . . . . . . 12 $/\$ $/\$
253	242, 251, 252	sylancr 668	. . . . . . . . . . 11
254		imaundi 5265	. . . . . . . . . . . . 13
255	47	imaeq2d 5185	. . . . . . . . . . . . . 14