poimirlem13 - Mathbox for Brendan Leahy

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

Theorem poimirlem13 31946

Description: Lemma for poimir 31966- for at most one simplex associated with a shared face is the opposite vertex first on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1

**Assertion**
Ref	Expression
poimirlem13

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem poimirlem13 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . . . . 9
2	1	ad2antrr 731	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		poimirlem22.s	. . . . . . . 8 ..^
4		poimirlem22.1	. . . . . . . . 9
5	4	ad2antrr 731	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
6		simplrl 769	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7		simprl 763	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
8	2, 3, 5, 6, 7	poimirlem10 31943	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
9		simplrr 770	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		simprr 765	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
11	2, 3, 5, 9, 10	poimirlem10 31943	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
12	8, 11	eqtr3d 2486	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		elrabi 3192	. . . . . . . . . . . . . 14 ..^ ..^
14	13, 3	eleq2s 2546	. . . . . . . . . . . . 13 ..^
15		xp1st 6820	. . . . . . . . . . . . 13 ..^ ..^
16	14, 15	syl 17	. . . . . . . . . . . 12 ..^
17		xp2nd 6821	. . . . . . . . . . . 12 ..^
18	16, 17	syl 17	. . . . . . . . . . 11
19		fvex 5873	. . . . . . . . . . . 12
20		f1oeq1 5803	. . . . . . . . . . . 12
21	19, 20	elab 3184	. . . . . . . . . . 11
22	18, 21	sylib 200	. . . . . . . . . 10
23		f1ofn 5813	. . . . . . . . . 10
24	22, 23	syl 17	. . . . . . . . 9
25	24	adantr 467	. . . . . . . 8 $/\$
26	25	ad2antlr 732	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
27		elrabi 3192	. . . . . . . . . . . . . 14 ..^ ..^
28	27, 3	eleq2s 2546	. . . . . . . . . . . . 13 ..^
29		xp1st 6820	. . . . . . . . . . . . 13 ..^ ..^
30	28, 29	syl 17	. . . . . . . . . . . 12 ..^
31		xp2nd 6821	. . . . . . . . . . . 12 ..^
32	30, 31	syl 17	. . . . . . . . . . 11
33		fvex 5873	. . . . . . . . . . . 12
34		f1oeq1 5803	. . . . . . . . . . . 12
35	33, 34	elab 3184	. . . . . . . . . . 11
36	32, 35	sylib 200	. . . . . . . . . 10
37		f1ofn 5813	. . . . . . . . . 10
38	36, 37	syl 17	. . . . . . . . 9
39	38	adantl 468	. . . . . . . 8 $/\$
40	39	ad2antlr 732	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
41		eleq1 2516	. . . . . . . . . . . . 13
42	41	anbi2d 709	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		oveq2 6296	. . . . . . . . . . . . . 14
44	43	imaeq2d 5167	. . . . . . . . . . . . 13
45	43	imaeq2d 5167	. . . . . . . . . . . . 13
46	44, 45	eqeq12d 2465	. . . . . . . . . . . 12
47	42, 46	imbi12d 322	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	1	ad3antrrr 735	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
49	4	ad3antrrr 735	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		simpl 459	. . . . . . . . . . . . . 14 $/\$
51	50	ad3antlr 736	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
52		simplrl 769	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		simpr 463	. . . . . . . . . . . . . 14 $/\$
54	53	ad3antlr 736	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		simplrr 770	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
56		simpr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
57	48, 3, 49, 51, 52, 54, 55, 56	poimirlem11 31944	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
58	48, 3, 49, 54, 55, 51, 52, 56	poimirlem11 31944	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
59	57, 58	eqssd 3448	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
60	47, 59	chvarv 2106	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
61		simpll 759	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62		elfznn 11825	. . . . . . . . . . . . . . . . . . 19
63		nnm1nn0 10908	. . . . . . . . . . . . . . . . . . 19
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18
65	64	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
66	62	nncnd 10622	. . . . . . . . . . . . . . . . . . . 20
67		ax-1cn 9594	. . . . . . . . . . . . . . . . . . . 20
68		subeq0 9897	. . . . . . . . . . . . . . . . . . . 20 $/\$
69	66, 67, 68	sylancl 667	. . . . . . . . . . . . . . . . . . 19
70	69	necon3abid 2659	. . . . . . . . . . . . . . . . . 18
71	70	biimpar 488	. . . . . . . . . . . . . . . . 17 $/\$
72		elnnne0 10880	. . . . . . . . . . . . . . . . 17 $/\$
73	65, 71, 72	sylanbrc 669	. . . . . . . . . . . . . . . 16 $/\$
74	73	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	64	nn0red 10923	. . . . . . . . . . . . . . . . . 18
76	75	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
77	62	nnred 10621	. . . . . . . . . . . . . . . . . 18
78	77	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
79	1	nnred 10621	. . . . . . . . . . . . . . . . . 18
80	79	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
81	77	lem1d 10537	. . . . . . . . . . . . . . . . . 18
82	81	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
83		elfzle2 11800	. . . . . . . . . . . . . . . . . 18
84	83	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
85	76, 78, 80, 82, 84	letrd 9789	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantrr 722	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	1	nnzd 11036	. . . . . . . . . . . . . . . . 17
88		fznn 11860	. . . . . . . . . . . . . . . . 17 $/\$
89	87, 88	syl 17	. . . . . . . . . . . . . . . 16 $/\$
90	89	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
91	74, 86, 90	mpbir2and 932	. . . . . . . . . . . . . 14 $/\$ $/\$
92	61, 91	sylan 474	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		ovex 6316	. . . . . . . . . . . . . 14
94		eleq1 2516	. . . . . . . . . . . . . . . 16
95	94	anbi2d 709	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		oveq2 6296	. . . . . . . . . . . . . . . . 17
97	96	imaeq2d 5167	. . . . . . . . . . . . . . . 16
98	96	imaeq2d 5167	. . . . . . . . . . . . . . . 16
99	97, 98	eqeq12d 2465	. . . . . . . . . . . . . . 15
100	95, 99	imbi12d 322	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	93, 100, 59	vtocl 3099	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
102	92, 101	syldan 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	expr 619	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
104		ima0 5182	. . . . . . . . . . . . 13
105		ima0 5182	. . . . . . . . . . . . 13
106	104, 105	eqtr4i 2475	. . . . . . . . . . . 12
107		oveq1 6295	. . . . . . . . . . . . . . . 16
108		1m1e0 10675	. . . . . . . . . . . . . . . 16
109	107, 108	syl6eq 2500	. . . . . . . . . . . . . . 15
110	109	oveq2d 6304	. . . . . . . . . . . . . 14
111		fz10 11817	. . . . . . . . . . . . . 14
112	110, 111	syl6eq 2500	. . . . . . . . . . . . 13
113	112	imaeq2d 5167	. . . . . . . . . . . 12
114	112	imaeq2d 5167	. . . . . . . . . . . 12
115	106, 113, 114	3eqtr4a 2510	. . . . . . . . . . 11
116	103, 115	pm2.61d2 164	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
117	60, 116	difeq12d 3551	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
118		fnsnfv 5923	. . . . . . . . . . . 12 $/\$
119	24, 118	sylan 474	. . . . . . . . . . 11 $/\$
120	62	adantl 468	. . . . . . . . . . . . 13 $/\$
121		uncom 3577	. . . . . . . . . . . . . . . 16
122	121	difeq1i 3546	. . . . . . . . . . . . . . 15 $\$ $\$
123		difun2 3846	. . . . . . . . . . . . . . 15 $\$ $\$
124	122, 123	eqtri 2472	. . . . . . . . . . . . . 14 $\$ $\$
125		nncn 10614	. . . . . . . . . . . . . . . . . . 19
126		npcan1 10041	. . . . . . . . . . . . . . . . . . 19
127	125, 126	syl 17	. . . . . . . . . . . . . . . . . 18
128		elnnuz 11192	. . . . . . . . . . . . . . . . . . 19
129	128	biimpi 198	. . . . . . . . . . . . . . . . . 18
130	127, 129	eqeltrd 2528	. . . . . . . . . . . . . . . . 17
131	63	nn0zd 11035	. . . . . . . . . . . . . . . . . . . 20
132		uzid 11170	. . . . . . . . . . . . . . . . . . . 20
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . 19
134		peano2uz 11209	. . . . . . . . . . . . . . . . . . 19
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	127, 135	eqeltrrd 2529	. . . . . . . . . . . . . . . . 17
137		fzsplit2 11821	. . . . . . . . . . . . . . . . 17 $/\$
138	130, 136, 137	syl2anc 666	. . . . . . . . . . . . . . . 16
139	127	oveq1d 6303	. . . . . . . . . . . . . . . . . 18
140		nnz 10956	. . . . . . . . . . . . . . . . . . 19
141		fzsn 11837	. . . . . . . . . . . . . . . . . . 19
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18
143	139, 142	eqtrd 2484	. . . . . . . . . . . . . . . . 17
144	143	uneq2d 3587	. . . . . . . . . . . . . . . 16
145	138, 144	eqtrd 2484	. . . . . . . . . . . . . . 15
146	145	difeq1d 3549	. . . . . . . . . . . . . 14 $\$ $\$
147		nnre 10613	. . . . . . . . . . . . . . . 16
148		ltm1 10442	. . . . . . . . . . . . . . . . . 18
149		peano2rem 9938	. . . . . . . . . . . . . . . . . . 19
150		ltnle 9710	. . . . . . . . . . . . . . . . . . 19 $/\$
151	149, 150	mpancom 674	. . . . . . . . . . . . . . . . . 18
152	148, 151	mpbid 214	. . . . . . . . . . . . . . . . 17
153		elfzle2 11800	. . . . . . . . . . . . . . . . 17
154	152, 153	nsyl 125	. . . . . . . . . . . . . . . 16
155	147, 154	syl 17	. . . . . . . . . . . . . . 15
156		incom 3624	. . . . . . . . . . . . . . . . 17
157	156	eqeq1i 2455	. . . . . . . . . . . . . . . 16
158		disjsn 4031	. . . . . . . . . . . . . . . 16
159		disj3 3808	. . . . . . . . . . . . . . . 16 $\$
160	157, 158, 159	3bitr3i 279	. . . . . . . . . . . . . . 15 $\$
161	155, 160	sylib 200	. . . . . . . . . . . . . 14 $\$
162	124, 146, 161	3eqtr4a 2510	. . . . . . . . . . . . 13 $\$
163	120, 162	syl 17	. . . . . . . . . . . 12 $/\$ $\$
164	163	imaeq2d 5167	. . . . . . . . . . 11 $/\$ $\$
165		dff1o3 5818	. . . . . . . . . . . . . . 15 $/\$
166	165	simprbi 466	. . . . . . . . . . . . . 14
167	22, 166	syl 17	. . . . . . . . . . . . 13
168		imadif 5656	. . . . . . . . . . . . 13 $\$ $\$
169	167, 168	syl 17	. . . . . . . . . . . 12 $\$ $\$
170	169	adantr 467	. . . . . . . . . . 11 $/\$ $\$ $\$
171	119, 164, 170	3eqtr2d 2490	. . . . . . . . . 10 $/\$ $\$
172	6, 171	sylan 474	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
173		eleq1 2516	. . . . . . . . . . . . 13
174	173	anbi1d 710	. . . . . . . . . . . 12 $/\$ $/\$
175		fveq2 5863	. . . . . . . . . . . . . . . 16
176	175	fveq2d 5867	. . . . . . . . . . . . . . 15
177	176	fveq1d 5865	. . . . . . . . . . . . . 14
178	177	sneqd 3979	. . . . . . . . . . . . 13
179	176	imaeq1d 5166	. . . . . . . . . . . . . 14
180	176	imaeq1d 5166	. . . . . . . . . . . . . 14
181	179, 180	difeq12d 3551	. . . . . . . . . . . . 13 $\$ $\$
182	178, 181	eqeq12d 2465	. . . . . . . . . . . 12 $\$ $\$
183	174, 182	imbi12d 322	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
184	183, 171	chvarv 2106	. . . . . . . . . 10 $/\$ $\$
185	9, 184	sylan 474	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
186	117, 172, 185	3eqtr4d 2494	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
187		fvex 5873	. . . . . . . . 9
188	187	sneqr 4138	. . . . . . . 8
189	186, 188	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	26, 40, 189	eqfnfvd 5977	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191		xpopth 6829	. . . . . . . 8 ..^ $/\$ ..^ $/\$
192	16, 30, 191	syl2an 480	. . . . . . 7 $/\$ $/\$
193	192	ad2antlr 732	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
194	12, 190, 193	mpbi2and 931	. . . . 5 $/\$ $/\$ $/\$ $/\$
195		eqtr3 2471	. . . . . 6 $/\$
196	195	adantl 468	. . . . 5 $/\$ $/\$ $/\$ $/\$
197		xpopth 6829	. . . . . . 7 ..^ $/\$ ..^ $/\$
198	14, 28, 197	syl2an 480	. . . . . 6 $/\$ $/\$
199	198	ad2antlr 732	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
200	194, 196, 199	mpbi2and 931	. . . 4 $/\$ $/\$ $/\$ $/\$
201	200	ex 436	. . 3 $/\$ $/\$ $/\$
202	201	ralrimivva 2808	. 2 $/\$
203		fveq2 5863	. . . 4
204	203	eqeq1d 2452	. . 3
205	204	rmo4 3230	. 2 $/\$
206	202, 205	sylibr 216	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1443

wcel 1886

cab 2436

wne 2621

wral 2736

wrmo 2739

crab 2740

csb 3362 $\$ cdif 3400

cun 3401

cin 3402

c0 3730

cif 3880

csn 3967 class class class wbr 4401

cmpt 4460

cxp 4831

ccnv 4832

cima 4836

wfun 5575

wfn 5576

wf 5577

wfo 5579

wf1o 5580

cfv 5581 (class class class)co 6288

cof 6526

c1st 6788

c2nd 6789

cmap 7469

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

clt 9672

cle 9673

cmin 9857

cn 10606

cn0 10866

cz 10934

cuz 11156

cfz 11781 ..^cfzo 11912

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-map 7471 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782 df-fzo 11913

This theorem is referenced by: poimirlem18 31951 poimirlem21 31954

W3C validator