poimirlem13 - Mathbox for Brendan Leahy

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

Theorem poimirlem13 31873

Description: Lemma for poimir 31893- 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 31870	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
9		simplrr 770	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		simprr 765	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
11	2, 3, 5, 9, 10	poimirlem10 31870	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
12	8, 11	eqtr3d 2466	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		elrabi 3227	. . . . . . . . . . . . . 14 ..^ ..^
14	13, 3	eleq2s 2531	. . . . . . . . . . . . 13 ..^
15		xp1st 6835	. . . . . . . . . . . . 13 ..^ ..^
16	14, 15	syl 17	. . . . . . . . . . . 12 ..^
17		xp2nd 6836	. . . . . . . . . . . 12 ..^
18	16, 17	syl 17	. . . . . . . . . . 11
19		fvex 5889	. . . . . . . . . . . 12
20		f1oeq1 5820	. . . . . . . . . . . 12
21	19, 20	elab 3219	. . . . . . . . . . 11
22	18, 21	sylib 200	. . . . . . . . . 10
23		f1ofn 5830	. . . . . . . . . 10
24	22, 23	syl 17	. . . . . . . . 9
25	24	adantr 467	. . . . . . . 8 $/\$
26	25	ad2antlr 732	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
27		elrabi 3227	. . . . . . . . . . . . . 14 ..^ ..^
28	27, 3	eleq2s 2531	. . . . . . . . . . . . 13 ..^
29		xp1st 6835	. . . . . . . . . . . . 13 ..^ ..^
30	28, 29	syl 17	. . . . . . . . . . . 12 ..^
31		xp2nd 6836	. . . . . . . . . . . 12 ..^
32	30, 31	syl 17	. . . . . . . . . . 11
33		fvex 5889	. . . . . . . . . . . 12
34		f1oeq1 5820	. . . . . . . . . . . 12
35	33, 34	elab 3219	. . . . . . . . . . 11
36	32, 35	sylib 200	. . . . . . . . . 10
37		f1ofn 5830	. . . . . . . . . 10
38	36, 37	syl 17	. . . . . . . . 9
39	38	adantl 468	. . . . . . . 8 $/\$
40	39	ad2antlr 732	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
41		eleq1 2495	. . . . . . . . . . . . 13
42	41	anbi2d 709	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		oveq2 6311	. . . . . . . . . . . . . 14
44	43	imaeq2d 5185	. . . . . . . . . . . . 13
45	43	imaeq2d 5185	. . . . . . . . . . . . 13
46	44, 45	eqeq12d 2445	. . . . . . . . . . . 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 31871	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
58	48, 3, 49, 54, 55, 51, 52, 56	poimirlem11 31871	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
59	57, 58	eqssd 3482	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
60	47, 59	chvarv 2069	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
61		simpll 759	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62		elfznn 11830	. . . . . . . . . . . . . . . . . . 19
63		nnm1nn0 10913	. . . . . . . . . . . . . . . . . . 19
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18
65	64	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
66	62	nncnd 10627	. . . . . . . . . . . . . . . . . . . 20
67		ax-1cn 9599	. . . . . . . . . . . . . . . . . . . 20
68		subeq0 9902	. . . . . . . . . . . . . . . . . . . 20 $/\$
69	66, 67, 68	sylancl 667	. . . . . . . . . . . . . . . . . . 19
70	69	necon3abid 2671	. . . . . . . . . . . . . . . . . 18
71	70	biimpar 488	. . . . . . . . . . . . . . . . 17 $/\$
72		elnnne0 10885	. . . . . . . . . . . . . . . . 17 $/\$
73	65, 71, 72	sylanbrc 669	. . . . . . . . . . . . . . . 16 $/\$
74	73	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	64	nn0red 10928	. . . . . . . . . . . . . . . . . 18
76	75	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
77	62	nnred 10626	. . . . . . . . . . . . . . . . . 18
78	77	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
79	1	nnred 10626	. . . . . . . . . . . . . . . . . 18
80	79	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
81	77	lem1d 10542	. . . . . . . . . . . . . . . . . 18
82	81	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
83		elfzle2 11805	. . . . . . . . . . . . . . . . . 18
84	83	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
85	76, 78, 80, 82, 84	letrd 9794	. . . . . . . . . . . . . . . 16 $/\$
86	85	adantrr 722	. . . . . . . . . . . . . . 15 $/\$ $/\$
87	1	nnzd 11041	. . . . . . . . . . . . . . . . 17
88		fznn 11865	. . . . . . . . . . . . . . . . 17 $/\$
89	87, 88	syl 17	. . . . . . . . . . . . . . . 16 $/\$
90	89	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
91	74, 86, 90	mpbir2and 931	. . . . . . . . . . . . . 14 $/\$ $/\$
92	61, 91	sylan 474	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		ovex 6331	. . . . . . . . . . . . . 14
94		eleq1 2495	. . . . . . . . . . . . . . . 16
95	94	anbi2d 709	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96		oveq2 6311	. . . . . . . . . . . . . . . . 17
97	96	imaeq2d 5185	. . . . . . . . . . . . . . . 16
98	96	imaeq2d 5185	. . . . . . . . . . . . . . . 16
99	97, 98	eqeq12d 2445	. . . . . . . . . . . . . . 15
100	95, 99	imbi12d 322	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	93, 100, 59	vtocl 3134	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
102	92, 101	syldan 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	expr 619	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
104		ima0 5200	. . . . . . . . . . . . 13
105		ima0 5200	. . . . . . . . . . . . 13
106	104, 105	eqtr4i 2455	. . . . . . . . . . . 12
107		oveq1 6310	. . . . . . . . . . . . . . . 16
108		1m1e0 10680	. . . . . . . . . . . . . . . 16
109	107, 108	syl6eq 2480	. . . . . . . . . . . . . . 15
110	109	oveq2d 6319	. . . . . . . . . . . . . 14
111		fz10 11822	. . . . . . . . . . . . . 14
112	110, 111	syl6eq 2480	. . . . . . . . . . . . 13
113	112	imaeq2d 5185	. . . . . . . . . . . 12
114	112	imaeq2d 5185	. . . . . . . . . . . 12
115	106, 113, 114	3eqtr4a 2490	. . . . . . . . . . 11
116	103, 115	pm2.61d2 164	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
117	60, 116	difeq12d 3585	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
118		fnsnfv 5939	. . . . . . . . . . . 12 $/\$
119	24, 118	sylan 474	. . . . . . . . . . 11 $/\$
120	62	adantl 468	. . . . . . . . . . . . 13 $/\$
121		uncom 3611	. . . . . . . . . . . . . . . 16
122	121	difeq1i 3580	. . . . . . . . . . . . . . 15 $\$ $\$
123		difun2 3876	. . . . . . . . . . . . . . 15 $\$ $\$
124	122, 123	eqtri 2452	. . . . . . . . . . . . . 14 $\$ $\$
125		nncn 10619	. . . . . . . . . . . . . . . . . . 19
126		npcan1 10046	. . . . . . . . . . . . . . . . . . 19
127	125, 126	syl 17	. . . . . . . . . . . . . . . . . 18
128		elnnuz 11197	. . . . . . . . . . . . . . . . . . 19
129	128	biimpi 198	. . . . . . . . . . . . . . . . . 18
130	127, 129	eqeltrd 2511	. . . . . . . . . . . . . . . . 17
131	63	nn0zd 11040	. . . . . . . . . . . . . . . . . . . 20
132		uzid 11175	. . . . . . . . . . . . . . . . . . . 20
133	131, 132	syl 17	. . . . . . . . . . . . . . . . . . 19
134		peano2uz 11214	. . . . . . . . . . . . . . . . . . 19
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18
136	127, 135	eqeltrrd 2512	. . . . . . . . . . . . . . . . 17
137		fzsplit2 11826	. . . . . . . . . . . . . . . . 17 $/\$
138	130, 136, 137	syl2anc 666	. . . . . . . . . . . . . . . 16
139	127	oveq1d 6318	. . . . . . . . . . . . . . . . . 18
140		nnz 10961	. . . . . . . . . . . . . . . . . . 19
141		fzsn 11842	. . . . . . . . . . . . . . . . . . 19
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18
143	139, 142	eqtrd 2464	. . . . . . . . . . . . . . . . 17
144	143	uneq2d 3621	. . . . . . . . . . . . . . . 16
145	138, 144	eqtrd 2464	. . . . . . . . . . . . . . 15
146	145	difeq1d 3583	. . . . . . . . . . . . . 14 $\$ $\$
147		nnre 10618	. . . . . . . . . . . . . . . 16
148		ltm1 10447	. . . . . . . . . . . . . . . . . 18
149		peano2rem 9943	. . . . . . . . . . . . . . . . . . 19
150		ltnle 9715	. . . . . . . . . . . . . . . . . . 19 $/\$
151	149, 150	mpancom 674	. . . . . . . . . . . . . . . . . 18
152	148, 151	mpbid 214	. . . . . . . . . . . . . . . . 17
153		elfzle2 11805	. . . . . . . . . . . . . . . . 17
154	152, 153	nsyl 125	. . . . . . . . . . . . . . . 16
155	147, 154	syl 17	. . . . . . . . . . . . . . 15
156		incom 3656	. . . . . . . . . . . . . . . . 17
157	156	eqeq1i 2430	. . . . . . . . . . . . . . . 16
158		disjsn 4058	. . . . . . . . . . . . . . . 16
159		disj3 3838	. . . . . . . . . . . . . . . 16 $\$
160	157, 158, 159	3bitr3i 279	. . . . . . . . . . . . . . 15 $\$
161	155, 160	sylib 200	. . . . . . . . . . . . . 14 $\$
162	124, 146, 161	3eqtr4a 2490	. . . . . . . . . . . . 13 $\$
163	120, 162	syl 17	. . . . . . . . . . . 12 $/\$ $\$
164	163	imaeq2d 5185	. . . . . . . . . . 11 $/\$ $\$
165		dff1o3 5835	. . . . . . . . . . . . . . 15 $/\$
166	165	simprbi 466	. . . . . . . . . . . . . 14
167	22, 166	syl 17	. . . . . . . . . . . . 13
168		imadif 5674	. . . . . . . . . . . . 13 $\$ $\$
169	167, 168	syl 17	. . . . . . . . . . . 12 $\$ $\$
170	169	adantr 467	. . . . . . . . . . 11 $/\$ $\$ $\$
171	119, 164, 170	3eqtr2d 2470	. . . . . . . . . 10 $/\$ $\$
172	6, 171	sylan 474	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
173		eleq1 2495	. . . . . . . . . . . . 13
174	173	anbi1d 710	. . . . . . . . . . . 12 $/\$ $/\$
175		fveq2 5879	. . . . . . . . . . . . . . . 16
176	175	fveq2d 5883	. . . . . . . . . . . . . . 15
177	176	fveq1d 5881	. . . . . . . . . . . . . 14
178	177	sneqd 4009	. . . . . . . . . . . . 13
179	176	imaeq1d 5184	. . . . . . . . . . . . . 14
180	176	imaeq1d 5184	. . . . . . . . . . . . . 14
181	179, 180	difeq12d 3585	. . . . . . . . . . . . 13 $\$ $\$
182	178, 181	eqeq12d 2445	. . . . . . . . . . . 12 $\$ $\$
183	174, 182	imbi12d 322	. . . . . . . . . . 11 $/\$ $\$ $/\$ $\$
184	183, 171	chvarv 2069	. . . . . . . . . 10 $/\$ $\$
185	9, 184	sylan 474	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
186	117, 172, 185	3eqtr4d 2474	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
187		fvex 5889	. . . . . . . . 9
188	187	sneqr 4165	. . . . . . . 8
189	186, 188	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
190	26, 40, 189	eqfnfvd 5992	. . . . . 6 $/\$ $/\$ $/\$ $/\$
191		xpopth 6844	. . . . . . . 8 ..^ $/\$ ..^ $/\$
192	16, 30, 191	syl2an 480	. . . . . . 7 $/\$ $/\$
193	192	ad2antlr 732	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
194	12, 190, 193	mpbi2and 930	. . . . 5 $/\$ $/\$ $/\$ $/\$
195		eqtr3 2451	. . . . . 6 $/\$
196	195	adantl 468	. . . . 5 $/\$ $/\$ $/\$ $/\$
197		xpopth 6844	. . . . . . 7 ..^ $/\$ ..^ $/\$
198	14, 28, 197	syl2an 480	. . . . . 6 $/\$ $/\$
199	198	ad2antlr 732	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
200	194, 196, 199	mpbi2and 930	. . . 4 $/\$ $/\$ $/\$ $/\$
201	200	ex 436	. . 3 $/\$ $/\$ $/\$
202	201	ralrimivva 2847	. 2 $/\$
203		fveq2 5879	. . . 4
204	203	eqeq1d 2425	. . 3
205	204	rmo4 3265	. 2 $/\$
206	202, 205	sylibr 216	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1438

wcel 1869

cab 2408

wne 2619

wral 2776

wrmo 2779

crab 2780

csb 3396 $\$ cdif 3434

cun 3435

cin 3436

c0 3762

cif 3910

csn 3997 class class class wbr 4421

cmpt 4480

cxp 4849

ccnv 4850

cima 4854

wfun 5593

wfn 5594

wf 5595

wfo 5597

wf1o 5598

cfv 5599 (class class class)co 6303

cof 6541

c1st 6803

c2nd 6804

cmap 7478

cc 9539

cr 9540

cc0 9541

c1 9542

caddc 9544

clt 9677

cle 9678

cmin 9862

cn 10611

cn0 10871

cz 10939

cuz 11161

cfz 11786 ..^cfzo 11917

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-rep 4534 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rmo 2784 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-tp 4002 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-tr 4517 df-eprel 4762 df-id 4766 df-po 4772 df-so 4773 df-fr 4810 df-we 4812 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-pred 5397 df-ord 5443 df-on 5444 df-lim 5445 df-suc 5446 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-of 6543 df-om 6705 df-1st 6805 df-2nd 6806 df-wrecs 7034 df-recs 7096 df-rdg 7134 df-er 7369 df-map 7480 df-en 7576 df-dom 7577 df-sdom 7578 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-nn 10612 df-n0 10872 df-z 10940 df-uz 11162 df-fz 11787 df-fzo 11918

This theorem is referenced by: poimirlem18 31878 poimirlem21 31881

W3C validator