poimirlem19 - Mathbox for Brendan Leahy

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

Theorem poimirlem19 31879

Description: Lemma for poimir 31893 establishing the vertices of the simplex in poimirlem20 31880. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem22.2
poimirlem22.3	$/\$
poimirlem21.4

**Assertion**
Ref	Expression
poimirlem19

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem19**
Step	Hyp	Ref	Expression
1		poimirlem22.2	. . 3
2		fveq2 5879	. . . . . . . . . . 11
3	2	breq2d 4433	. . . . . . . . . 10
4	3	ifbid 3932	. . . . . . . . 9
5	4	csbeq1d 3403	. . . . . . . 8
6		fveq2 5879	. . . . . . . . . . 11
7	6	fveq2d 5883	. . . . . . . . . 10
8	6	fveq2d 5883	. . . . . . . . . . . . 13
9	8	imaeq1d 5184	. . . . . . . . . . . 12
10	9	xpeq1d 4874	. . . . . . . . . . 11
11	8	imaeq1d 5184	. . . . . . . . . . . 12
12	11	xpeq1d 4874	. . . . . . . . . . 11
13	10, 12	uneq12d 3622	. . . . . . . . . 10
14	7, 13	oveq12d 6321	. . . . . . . . 9
15	14	csbeq2dv 3810	. . . . . . . 8
16	5, 15	eqtrd 2464	. . . . . . 7
17	16	mpteq2dv 4509	. . . . . 6
18	17	eqeq2d 2437	. . . . 5
19		poimirlem22.s	. . . . 5 ..^
20	18, 19	elrab2 3232	. . . 4 ..^ $/\$
21	20	simprbi 466	. . 3
22	1, 21	syl 17	. 2
23		elrabi 3227	. . . . . . . . . . . 12 ..^ ..^
24	23, 19	eleq2s 2531	. . . . . . . . . . 11 ..^
25	1, 24	syl 17	. . . . . . . . . 10 ..^
26		xp1st 6835	. . . . . . . . . 10 ..^ ..^
27	25, 26	syl 17	. . . . . . . . 9 ..^
28		xp1st 6835	. . . . . . . . 9 ..^ ..^
29	27, 28	syl 17	. . . . . . . 8 ..^
30		elmapfn 7500	. . . . . . . 8 ..^
31	29, 30	syl 17	. . . . . . 7
32	31	adantr 467	. . . . . 6 $/\$
33		1ex 9640	. . . . . . . . . 10
34		fnconstg 5786	. . . . . . . . . 10
35	33, 34	ax-mp 5	. . . . . . . . 9
36		c0ex 9639	. . . . . . . . . 10
37		fnconstg 5786	. . . . . . . . . 10
38	36, 37	ax-mp 5	. . . . . . . . 9
39	35, 38	pm3.2i 457	. . . . . . . 8 $/\$
40		xp2nd 6836	. . . . . . . . . . . . 13 ..^
41	27, 40	syl 17	. . . . . . . . . . . 12
42		fvex 5889	. . . . . . . . . . . . 13
43		f1oeq1 5820	. . . . . . . . . . . . 13
44	42, 43	elab 3219	. . . . . . . . . . . 12
45	41, 44	sylib 200	. . . . . . . . . . 11
46		dff1o3 5835	. . . . . . . . . . . 12 $/\$
47	46	simprbi 466	. . . . . . . . . . 11
48	45, 47	syl 17	. . . . . . . . . 10
49		imain 5675	. . . . . . . . . 10
50	48, 49	syl 17	. . . . . . . . 9
51		elfznn0 11889	. . . . . . . . . . . . . 14
52	51	nn0red 10928	. . . . . . . . . . . . 13
53	52	ltp1d 10539	. . . . . . . . . . . 12
54		fzdisj 11828	. . . . . . . . . . . 12
55	53, 54	syl 17	. . . . . . . . . . 11
56	55	imaeq2d 5185	. . . . . . . . . 10
57		ima0 5200	. . . . . . . . . 10
58	56, 57	syl6eq 2480	. . . . . . . . 9
59	50, 58	sylan9req 2485	. . . . . . . 8 $/\$
60		fnun 5698	. . . . . . . 8 $/\$ $/\$
61	39, 59, 60	sylancr 668	. . . . . . 7 $/\$
62		imaundi 5265	. . . . . . . . 9
63		nn0p1nn 10911	. . . . . . . . . . . . . . 15
64	51, 63	syl 17	. . . . . . . . . . . . . 14
65		nnuz 11196	. . . . . . . . . . . . . 14
66	64, 65	syl6eleq 2521	. . . . . . . . . . . . 13
67	66	adantl 468	. . . . . . . . . . . 12 $/\$
68		poimir.0	. . . . . . . . . . . . . . . 16
69	68	nncnd 10627	. . . . . . . . . . . . . . 15
70		npcan1 10046	. . . . . . . . . . . . . . 15
71	69, 70	syl 17	. . . . . . . . . . . . . 14
72	71	adantr 467	. . . . . . . . . . . . 13 $/\$
73		elfzuz3 11799	. . . . . . . . . . . . . . 15
74		peano2uz 11214	. . . . . . . . . . . . . . 15
75	73, 74	syl 17	. . . . . . . . . . . . . 14
76	75	adantl 468	. . . . . . . . . . . . 13 $/\$
77	72, 76	eqeltrrd 2512	. . . . . . . . . . . 12 $/\$
78		fzsplit2 11826	. . . . . . . . . . . 12 $/\$
79	67, 77, 78	syl2anc 666	. . . . . . . . . . 11 $/\$
80	79	imaeq2d 5185	. . . . . . . . . 10 $/\$
81		f1ofo 5836	. . . . . . . . . . . 12
82		foima 5813	. . . . . . . . . . . 12
83	45, 81, 82	3syl 18	. . . . . . . . . . 11
84	83	adantr 467	. . . . . . . . . 10 $/\$
85	80, 84	eqtr3d 2466	. . . . . . . . 9 $/\$
86	62, 85	syl5eqr 2478	. . . . . . . 8 $/\$
87	86	fneq2d 5683	. . . . . . 7 $/\$
88	61, 87	mpbid 214	. . . . . 6 $/\$
89		ovex 6331	. . . . . . 7
90	89	a1i 11	. . . . . 6 $/\$
91		inidm 3672	. . . . . 6
92		eqidd 2424	. . . . . 6 $/\$ $/\$
93		eqidd 2424	. . . . . 6 $/\$ $/\$
94	32, 88, 90, 90, 91, 92, 93	offval 6550	. . . . 5 $/\$
95		elmapi 7499	. . . . . . . . . . . . 13 ..^ ..^
96	29, 95	syl 17	. . . . . . . . . . . 12 ..^
97	96	ffvelrnda 6035	. . . . . . . . . . 11 $/\$ ..^
98		elfzonn0 11962	. . . . . . . . . . 11 ..^
99	97, 98	syl 17	. . . . . . . . . 10 $/\$
100	99	nn0cnd 10929	. . . . . . . . 9 $/\$
101	100	adantlr 720	. . . . . . . 8 $/\$ $/\$
102		ax-1cn 9599	. . . . . . . . . 10
103		0cn 9637	. . . . . . . . . 10
104	102, 103	keepel 3977	. . . . . . . . 9
105	104	a1i 11	. . . . . . . 8 $/\$ $/\$
106		snssi 4142	. . . . . . . . . . 11
107	102, 106	ax-mp 5	. . . . . . . . . 10
108		snssi 4142	. . . . . . . . . . 11
109	103, 108	ax-mp 5	. . . . . . . . . 10
110	107, 109	unssi 3642	. . . . . . . . 9
111	33	fconst 5784	. . . . . . . . . . . . 13
112	36	fconst 5784	. . . . . . . . . . . . 13
113	111, 112	pm3.2i 457	. . . . . . . . . . . 12 $/\$
114		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
115	68	nnzd 11041	. . . . . . . . . . . . . . . . . . . . . . 23
116		1z 10969	. . . . . . . . . . . . . . . . . . . . . . . 24
117		peano2z 10980	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
119	115, 118	jctil 540	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
120		elfzelz 11802	. . . . . . . . . . . . . . . . . . . . . . 23
121	120, 116	jctir 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		fzsubel 11836	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
123	119, 121, 122	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	114, 123	mpbid 214	. . . . . . . . . . . . . . . . . . . 20 $/\$
125	102, 102	pncan3oi 9893	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 6313	. . . . . . . . . . . . . . . . . . . 20
127	124, 126	syl6eleq 2521	. . . . . . . . . . . . . . . . . . 19 $/\$
128	127	ralrimiva 2840	. . . . . . . . . . . . . . . . . 18
129		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
130		peano2zm 10982	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	115, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131, 116	jctil 540	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
133		elfzelz 11802	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133, 116	jctir 541	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		fzaddel 11835	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
136	132, 134, 135	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
137	129, 136	mpbid 214	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	71	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . 22
139	138	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	137, 139	eleqtrd 2513	. . . . . . . . . . . . . . . . . . . 20 $/\$
141	120	zcnd 11043	. . . . . . . . . . . . . . . . . . . . . . 23
142	133	zcnd 11043	. . . . . . . . . . . . . . . . . . . . . . 23
143		subadd2 9881	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
144	102, 143	mp3an2 1349	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
145		eqcom 2432	. . . . . . . . . . . . . . . . . . . . . . . 24
146		eqcom 2432	. . . . . . . . . . . . . . . . . . . . . . . 24
147	144, 145, 146	3bitr4g 292	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
148	141, 142, 147	syl2anr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
149	148	ralrimiva 2840	. . . . . . . . . . . . . . . . . . . . 21
150	149	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
151		reu6i 3263	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	140, 150, 151	syl2anc 666	. . . . . . . . . . . . . . . . . . 19 $/\$
153	152	ralrimiva 2840	. . . . . . . . . . . . . . . . . 18
154		eqid 2423	. . . . . . . . . . . . . . . . . . 19
155	154	f1ompt 6057	. . . . . . . . . . . . . . . . . 18 $/\$
156	128, 153, 155	sylanbrc 669	. . . . . . . . . . . . . . . . 17
157		f1osng 5867	. . . . . . . . . . . . . . . . . 18 $/\$
158	33, 68, 157	sylancr 668	. . . . . . . . . . . . . . . . 17
159	68	nnred 10626	. . . . . . . . . . . . . . . . . . . . 21
160	159	ltm1d 10541	. . . . . . . . . . . . . . . . . . . 20
161	131	zred 11042	. . . . . . . . . . . . . . . . . . . . 21
162	161, 159	ltnled 9784	. . . . . . . . . . . . . . . . . . . 20
163	160, 162	mpbid 214	. . . . . . . . . . . . . . . . . . 19
164		elfzle2 11805	. . . . . . . . . . . . . . . . . . 19
165	163, 164	nsyl 125	. . . . . . . . . . . . . . . . . 18
166		disjsn 4058	. . . . . . . . . . . . . . . . . 18
167	165, 166	sylibr 216	. . . . . . . . . . . . . . . . 17
168		1re 9644	. . . . . . . . . . . . . . . . . . . . . 22
169	168	ltp1i 10512	. . . . . . . . . . . . . . . . . . . . 21
170	118	zrei 10945	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	ltnlei 9757	. . . . . . . . . . . . . . . . . . . . 21
172	169, 171	mpbi 212	. . . . . . . . . . . . . . . . . . . 20
173		elfzle1 11804	. . . . . . . . . . . . . . . . . . . 20
174	172, 173	mto 180	. . . . . . . . . . . . . . . . . . 19
175		disjsn 4058	. . . . . . . . . . . . . . . . . . 19
176	174, 175	mpbir 213	. . . . . . . . . . . . . . . . . 18
177		f1oun 5848	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
178	176, 177	mpanr1 688	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
179	156, 158, 167, 178	syl21anc 1264	. . . . . . . . . . . . . . . 16
180		eleq1 2495	. . . . . . . . . . . . . . . . . . . . . . 23
181	174, 180	mtbiri 305	. . . . . . . . . . . . . . . . . . . . . 22
182	181	necon2ai 2660	. . . . . . . . . . . . . . . . . . . . 21
183		ifnefalse 3922	. . . . . . . . . . . . . . . . . . . . 21
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . 20
185	184	mpteq2ia 4504	. . . . . . . . . . . . . . . . . . 19
186	185	uneq1i 3617	. . . . . . . . . . . . . . . . . 18
187	33	a1i 11	. . . . . . . . . . . . . . . . . . 19
188		ssv 3485	. . . . . . . . . . . . . . . . . . . 20
189	188, 68	sseldi 3463	. . . . . . . . . . . . . . . . . . 19
190	68, 65	syl6eleq 2521	. . . . . . . . . . . . . . . . . . . . 21
191		fzpred 11846	. . . . . . . . . . . . . . . . . . . . 21
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . 20
193		uncom 3611	. . . . . . . . . . . . . . . . . . . 20
194	192, 193	syl6req 2481	. . . . . . . . . . . . . . . . . . 19
195		iftrue 3916	. . . . . . . . . . . . . . . . . . . 20
196	195	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
197	187, 189, 194, 196	fmptapd 6101	. . . . . . . . . . . . . . . . . 18
198	186, 197	syl5eqr 2478	. . . . . . . . . . . . . . . . 17
199	71, 190	eqeltrd 2511	. . . . . . . . . . . . . . . . . . 19
200		uzid 11175	. . . . . . . . . . . . . . . . . . . . 21
201		peano2uz 11214	. . . . . . . . . . . . . . . . . . . . 21
202	131, 200, 201	3syl 18	. . . . . . . . . . . . . . . . . . . 20
203	71, 202	eqeltrrd 2512	. . . . . . . . . . . . . . . . . . 19
204		fzsplit2 11826	. . . . . . . . . . . . . . . . . . 19 $/\$
205	199, 203, 204	syl2anc 666	. . . . . . . . . . . . . . . . . 18
206	71	oveq1d 6318	. . . . . . . . . . . . . . . . . . . 20
207		fzsn 11842	. . . . . . . . . . . . . . . . . . . . 21
208	115, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20
209	206, 208	eqtrd 2464	. . . . . . . . . . . . . . . . . . 19
210	209	uneq2d 3621	. . . . . . . . . . . . . . . . . 18
211	205, 210	eqtr2d 2465	. . . . . . . . . . . . . . . . 17
212	198, 194, 211	f1oeq123d 5826	. . . . . . . . . . . . . . . 16
213	179, 212	mpbid 214	. . . . . . . . . . . . . . 15
214		f1oco 5851	. . . . . . . . . . . . . . 15 $/\$
215	45, 213, 214	syl2anc 666	. . . . . . . . . . . . . 14
216		dff1o3 5835	. . . . . . . . . . . . . . 15 $/\$
217	216	simprbi 466	. . . . . . . . . . . . . 14
218		imain 5675	. . . . . . . . . . . . . 14
219	215, 217, 218	3syl 18	. . . . . . . . . . . . 13
220	64	nnred 10626	. . . . . . . . . . . . . . . . 17
221	220	ltp1d 10539	. . . . . . . . . . . . . . . 16
222		fzdisj 11828	. . . . . . . . . . . . . . . 16
223	221, 222	syl 17	. . . . . . . . . . . . . . 15
224	223	imaeq2d 5185	. . . . . . . . . . . . . 14
225		ima0 5200	. . . . . . . . . . . . . 14
226	224, 225	syl6eq 2480	. . . . . . . . . . . . 13
227	219, 226	sylan9req 2485	. . . . . . . . . . . 12 $/\$
228		fun 5761	. . . . . . . . . . . 12 $/\$ $/\$
229	113, 227, 228	sylancr 668	. . . . . . . . . . 11 $/\$
230		imaundi 5265	. . . . . . . . . . . . 13
231	64	peano2nnd 10628	. . . . . . . . . . . . . . . . . 18
232	231, 65	syl6eleq 2521	. . . . . . . . . . . . . . . . 17
233	232	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
234		eluzp1p1 11186	. . . . . . . . . . . . . . . . . . 19
235	73, 234	syl 17	. . . . . . . . . . . . . . . . . 18
236	235	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
237	72, 236	eqeltrrd 2512	. . . . . . . . . . . . . . . 16 $/\$
238		fzsplit2 11826	. . . . . . . . . . . . . . . 16 $/\$
239	233, 237, 238	syl2anc 666	. . . . . . . . . . . . . . 15 $/\$
240	239	imaeq2d 5185	. . . . . . . . . . . . . 14 $/\$
241		f1ofo 5836	. . . . . . . . . . . . . . . 16
242		foima 5813	. . . . . . . . . . . . . . . 16
243	215, 241, 242	3syl 18	. . . . . . . . . . . . . . 15
244	243	adantr 467	. . . . . . . . . . . . . 14 $/\$
245	240, 244	eqtr3d 2466	. . . . . . . . . . . . 13 $/\$
246	230, 245	syl5eqr 2478	. . . . . . . . . . . 12 $/\$
247	246	feq2d 5731	. . . . . . . . . . 11 $/\$
248	229, 247	mpbid 214	. . . . . . . . . 10 $/\$
249	248	ffvelrnda 6035	. . . . . . . . 9 $/\$ $/\$
250	110, 249	sseldi 3463	. . . . . . . 8 $/\$ $/\$
251	101, 105, 250	subadd23d 10010	. . . . . . 7 $/\$ $/\$
252		oveq2 6311	. . . . . . . . . 10
253	252	eqeq1d 2425	. . . . . . . . 9
254		oveq2 6311	. . . . . . . . . 10
255	254	eqeq1d 2425	. . . . . . . . 9
256		1m1e0 10680	. . . . . . . . . . . . 13
257		f1ofn 5830	. . . . . . . . . . . . . . . . . . . 20
258	45, 257	syl 17	. . . . . . . . . . . . . . . . . . 19
259	258	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
260		imassrn 5196	. . . . . . . . . . . . . . . . . . . 20
261		f1of 5829	. . . . . . . . . . . . . . . . . . . . . 22
262	213, 261	syl 17	. . . . . . . . . . . . . . . . . . . . 21
263		frn 5750	. . . . . . . . . . . . . . . . . . . . 21
264	262, 263	syl 17	. . . . . . . . . . . . . . . . . . . 20
265	260, 264	syl5ss 3476	. . . . . . . . . . . . . . . . . . 19