poimirlem19 - Mathbox for Brendan Leahy

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

Theorem poimirlem19 31959

Description: Lemma for poimir 31973 establishing the vertices of the simplex in poimirlem20 31960. (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 5865	. . . . . . . . . . 11
3	2	breq2d 4414	. . . . . . . . . 10
4	3	ifbid 3903	. . . . . . . . 9
5	4	csbeq1d 3370	. . . . . . . 8
6		fveq2 5865	. . . . . . . . . . 11
7	6	fveq2d 5869	. . . . . . . . . 10
8	6	fveq2d 5869	. . . . . . . . . . . . 13
9	8	imaeq1d 5167	. . . . . . . . . . . 12
10	9	xpeq1d 4857	. . . . . . . . . . 11
11	8	imaeq1d 5167	. . . . . . . . . . . 12
12	11	xpeq1d 4857	. . . . . . . . . . 11
13	10, 12	uneq12d 3589	. . . . . . . . . 10
14	7, 13	oveq12d 6308	. . . . . . . . 9
15	14	csbeq2dv 3781	. . . . . . . 8
16	5, 15	eqtrd 2485	. . . . . . 7
17	16	mpteq2dv 4490	. . . . . 6
18	17	eqeq2d 2461	. . . . 5
19		poimirlem22.s	. . . . 5 ..^
20	18, 19	elrab2 3198	. . . 4 ..^ $/\$
21	20	simprbi 466	. . 3
22	1, 21	syl 17	. 2
23		elrabi 3193	. . . . . . . . . . . 12 ..^ ..^
24	23, 19	eleq2s 2547	. . . . . . . . . . 11 ..^
25	1, 24	syl 17	. . . . . . . . . 10 ..^
26		xp1st 6823	. . . . . . . . . 10 ..^ ..^
27	25, 26	syl 17	. . . . . . . . 9 ..^
28		xp1st 6823	. . . . . . . . 9 ..^ ..^
29	27, 28	syl 17	. . . . . . . 8 ..^
30		elmapfn 7494	. . . . . . . 8 ..^
31	29, 30	syl 17	. . . . . . 7
32	31	adantr 467	. . . . . 6 $/\$
33		1ex 9638	. . . . . . . . . 10
34		fnconstg 5771	. . . . . . . . . 10
35	33, 34	ax-mp 5	. . . . . . . . 9
36		c0ex 9637	. . . . . . . . . 10
37		fnconstg 5771	. . . . . . . . . 10
38	36, 37	ax-mp 5	. . . . . . . . 9
39	35, 38	pm3.2i 457	. . . . . . . 8 $/\$
40		xp2nd 6824	. . . . . . . . . . . . 13 ..^
41	27, 40	syl 17	. . . . . . . . . . . 12
42		fvex 5875	. . . . . . . . . . . . 13
43		f1oeq1 5805	. . . . . . . . . . . . 13
44	42, 43	elab 3185	. . . . . . . . . . . 12
45	41, 44	sylib 200	. . . . . . . . . . 11
46		dff1o3 5820	. . . . . . . . . . . 12 $/\$
47	46	simprbi 466	. . . . . . . . . . 11
48	45, 47	syl 17	. . . . . . . . . 10
49		imain 5659	. . . . . . . . . 10
50	48, 49	syl 17	. . . . . . . . 9
51		elfznn0 11887	. . . . . . . . . . . . . 14
52	51	nn0red 10926	. . . . . . . . . . . . 13
53	52	ltp1d 10537	. . . . . . . . . . . 12
54		fzdisj 11826	. . . . . . . . . . . 12
55	53, 54	syl 17	. . . . . . . . . . 11
56	55	imaeq2d 5168	. . . . . . . . . 10
57		ima0 5183	. . . . . . . . . 10
58	56, 57	syl6eq 2501	. . . . . . . . 9
59	50, 58	sylan9req 2506	. . . . . . . 8 $/\$
60		fnun 5682	. . . . . . . 8 $/\$ $/\$
61	39, 59, 60	sylancr 669	. . . . . . 7 $/\$
62		imaundi 5248	. . . . . . . . 9
63		nn0p1nn 10909	. . . . . . . . . . . . . . 15
64	51, 63	syl 17	. . . . . . . . . . . . . 14
65		nnuz 11194	. . . . . . . . . . . . . 14
66	64, 65	syl6eleq 2539	. . . . . . . . . . . . 13
67	66	adantl 468	. . . . . . . . . . . 12 $/\$
68		poimir.0	. . . . . . . . . . . . . . . 16
69	68	nncnd 10625	. . . . . . . . . . . . . . 15
70		npcan1 10044	. . . . . . . . . . . . . . 15
71	69, 70	syl 17	. . . . . . . . . . . . . 14
72	71	adantr 467	. . . . . . . . . . . . 13 $/\$
73		elfzuz3 11797	. . . . . . . . . . . . . . 15
74		peano2uz 11212	. . . . . . . . . . . . . . 15
75	73, 74	syl 17	. . . . . . . . . . . . . 14
76	75	adantl 468	. . . . . . . . . . . . 13 $/\$
77	72, 76	eqeltrrd 2530	. . . . . . . . . . . 12 $/\$
78		fzsplit2 11824	. . . . . . . . . . . 12 $/\$
79	67, 77, 78	syl2anc 667	. . . . . . . . . . 11 $/\$
80	79	imaeq2d 5168	. . . . . . . . . 10 $/\$
81		f1ofo 5821	. . . . . . . . . . . 12
82		foima 5798	. . . . . . . . . . . 12
83	45, 81, 82	3syl 18	. . . . . . . . . . 11
84	83	adantr 467	. . . . . . . . . 10 $/\$
85	80, 84	eqtr3d 2487	. . . . . . . . 9 $/\$
86	62, 85	syl5eqr 2499	. . . . . . . 8 $/\$
87	86	fneq2d 5667	. . . . . . 7 $/\$
88	61, 87	mpbid 214	. . . . . 6 $/\$
89		ovex 6318	. . . . . . 7
90	89	a1i 11	. . . . . 6 $/\$
91		inidm 3641	. . . . . 6
92		eqidd 2452	. . . . . 6 $/\$ $/\$
93		eqidd 2452	. . . . . 6 $/\$ $/\$
94	32, 88, 90, 90, 91, 92, 93	offval 6538	. . . . 5 $/\$
95		elmapi 7493	. . . . . . . . . . . . 13 ..^ ..^
96	29, 95	syl 17	. . . . . . . . . . . 12 ..^
97	96	ffvelrnda 6022	. . . . . . . . . . 11 $/\$ ..^
98		elfzonn0 11960	. . . . . . . . . . 11 ..^
99	97, 98	syl 17	. . . . . . . . . 10 $/\$
100	99	nn0cnd 10927	. . . . . . . . 9 $/\$
101	100	adantlr 721	. . . . . . . 8 $/\$ $/\$
102		ax-1cn 9597	. . . . . . . . . 10
103		0cn 9635	. . . . . . . . . 10
104	102, 103	keepel 3948	. . . . . . . . 9
105	104	a1i 11	. . . . . . . 8 $/\$ $/\$
106		snssi 4116	. . . . . . . . . . 11
107	102, 106	ax-mp 5	. . . . . . . . . 10
108		snssi 4116	. . . . . . . . . . 11
109	103, 108	ax-mp 5	. . . . . . . . . 10
110	107, 109	unssi 3609	. . . . . . . . 9
111	33	fconst 5769	. . . . . . . . . . . . 13
112	36	fconst 5769	. . . . . . . . . . . . 13
113	111, 112	pm3.2i 457	. . . . . . . . . . . 12 $/\$
114		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
115	68	nnzd 11039	. . . . . . . . . . . . . . . . . . . . . . 23
116		1z 10967	. . . . . . . . . . . . . . . . . . . . . . . 24
117		peano2z 10978	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
119	115, 118	jctil 540	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
120		elfzelz 11800	. . . . . . . . . . . . . . . . . . . . . . 23
121	120, 116	jctir 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		fzsubel 11834	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
123	119, 121, 122	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	114, 123	mpbid 214	. . . . . . . . . . . . . . . . . . . 20 $/\$
125	102, 102	pncan3oi 9891	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 6300	. . . . . . . . . . . . . . . . . . . 20
127	124, 126	syl6eleq 2539	. . . . . . . . . . . . . . . . . . 19 $/\$
128	127	ralrimiva 2802	. . . . . . . . . . . . . . . . . 18
129		simpr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
130		peano2zm 10980	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	115, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131, 116	jctil 540	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
133		elfzelz 11800	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133, 116	jctir 541	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		fzaddel 11833	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
136	132, 134, 135	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
137	129, 136	mpbid 214	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	71	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . 22
139	138	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	137, 139	eleqtrd 2531	. . . . . . . . . . . . . . . . . . . 20 $/\$
141	120	zcnd 11041	. . . . . . . . . . . . . . . . . . . . . . 23
142	133	zcnd 11041	. . . . . . . . . . . . . . . . . . . . . . 23
143		subadd2 9879	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
144	102, 143	mp3an2 1352	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
145		eqcom 2458	. . . . . . . . . . . . . . . . . . . . . . . 24
146		eqcom 2458	. . . . . . . . . . . . . . . . . . . . . . . 24
147	144, 145, 146	3bitr4g 292	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
148	141, 142, 147	syl2anr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
149	148	ralrimiva 2802	. . . . . . . . . . . . . . . . . . . . 21
150	149	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
151		reu6i 3229	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	140, 150, 151	syl2anc 667	. . . . . . . . . . . . . . . . . . 19 $/\$
153	152	ralrimiva 2802	. . . . . . . . . . . . . . . . . 18
154		eqid 2451	. . . . . . . . . . . . . . . . . . 19
155	154	f1ompt 6044	. . . . . . . . . . . . . . . . . 18 $/\$
156	128, 153, 155	sylanbrc 670	. . . . . . . . . . . . . . . . 17
157		f1osng 5853	. . . . . . . . . . . . . . . . . 18 $/\$
158	33, 68, 157	sylancr 669	. . . . . . . . . . . . . . . . 17
159	68	nnred 10624	. . . . . . . . . . . . . . . . . . . . 21
160	159	ltm1d 10539	. . . . . . . . . . . . . . . . . . . 20
161	131	zred 11040	. . . . . . . . . . . . . . . . . . . . 21
162	161, 159	ltnled 9782	. . . . . . . . . . . . . . . . . . . 20
163	160, 162	mpbid 214	. . . . . . . . . . . . . . . . . . 19
164		elfzle2 11803	. . . . . . . . . . . . . . . . . . 19
165	163, 164	nsyl 125	. . . . . . . . . . . . . . . . . 18
166		disjsn 4032	. . . . . . . . . . . . . . . . . 18
167	165, 166	sylibr 216	. . . . . . . . . . . . . . . . 17
168		1re 9642	. . . . . . . . . . . . . . . . . . . . . 22
169	168	ltp1i 10510	. . . . . . . . . . . . . . . . . . . . 21
170	118	zrei 10943	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	ltnlei 9755	. . . . . . . . . . . . . . . . . . . . 21
172	169, 171	mpbi 212	. . . . . . . . . . . . . . . . . . . 20
173		elfzle1 11802	. . . . . . . . . . . . . . . . . . . 20
174	172, 173	mto 180	. . . . . . . . . . . . . . . . . . 19
175		disjsn 4032	. . . . . . . . . . . . . . . . . . 19
176	174, 175	mpbir 213	. . . . . . . . . . . . . . . . . 18
177		f1oun 5833	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
178	176, 177	mpanr1 689	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
179	156, 158, 167, 178	syl21anc 1267	. . . . . . . . . . . . . . . 16
180		eleq1 2517	. . . . . . . . . . . . . . . . . . . . . . 23
181	174, 180	mtbiri 305	. . . . . . . . . . . . . . . . . . . . . 22
182	181	necon2ai 2653	. . . . . . . . . . . . . . . . . . . . 21
183		ifnefalse 3893	. . . . . . . . . . . . . . . . . . . . 21
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . 20
185	184	mpteq2ia 4485	. . . . . . . . . . . . . . . . . . 19
186	185	uneq1i 3584	. . . . . . . . . . . . . . . . . 18
187	33	a1i 11	. . . . . . . . . . . . . . . . . . 19
188		ssv 3452	. . . . . . . . . . . . . . . . . . . 20
189	188, 68	sseldi 3430	. . . . . . . . . . . . . . . . . . 19
190	68, 65	syl6eleq 2539	. . . . . . . . . . . . . . . . . . . . 21
191		fzpred 11844	. . . . . . . . . . . . . . . . . . . . 21
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . 20
193		uncom 3578	. . . . . . . . . . . . . . . . . . . 20
194	192, 193	syl6req 2502	. . . . . . . . . . . . . . . . . . 19
195		iftrue 3887	. . . . . . . . . . . . . . . . . . . 20
196	195	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$
197	187, 189, 194, 196	fmptapd 6088	. . . . . . . . . . . . . . . . . 18
198	186, 197	syl5eqr 2499	. . . . . . . . . . . . . . . . 17
199	71, 190	eqeltrd 2529	. . . . . . . . . . . . . . . . . . 19
200		uzid 11173	. . . . . . . . . . . . . . . . . . . . 21
201		peano2uz 11212	. . . . . . . . . . . . . . . . . . . . 21
202	131, 200, 201	3syl 18	. . . . . . . . . . . . . . . . . . . 20
203	71, 202	eqeltrrd 2530	. . . . . . . . . . . . . . . . . . 19
204		fzsplit2 11824	. . . . . . . . . . . . . . . . . . 19 $/\$
205	199, 203, 204	syl2anc 667	. . . . . . . . . . . . . . . . . 18
206	71	oveq1d 6305	. . . . . . . . . . . . . . . . . . . 20
207		fzsn 11840	. . . . . . . . . . . . . . . . . . . . 21
208	115, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20
209	206, 208	eqtrd 2485	. . . . . . . . . . . . . . . . . . 19
210	209	uneq2d 3588	. . . . . . . . . . . . . . . . . 18
211	205, 210	eqtr2d 2486	. . . . . . . . . . . . . . . . 17
212	198, 194, 211	f1oeq123d 5811	. . . . . . . . . . . . . . . 16
213	179, 212	mpbid 214	. . . . . . . . . . . . . . 15
214		f1oco 5836	. . . . . . . . . . . . . . 15 $/\$
215	45, 213, 214	syl2anc 667	. . . . . . . . . . . . . 14
216		dff1o3 5820	. . . . . . . . . . . . . . 15 $/\$
217	216	simprbi 466	. . . . . . . . . . . . . 14
218		imain 5659	. . . . . . . . . . . . . 14
219	215, 217, 218	3syl 18	. . . . . . . . . . . . 13
220	64	nnred 10624	. . . . . . . . . . . . . . . . 17
221	220	ltp1d 10537	. . . . . . . . . . . . . . . 16
222		fzdisj 11826	. . . . . . . . . . . . . . . 16
223	221, 222	syl 17	. . . . . . . . . . . . . . 15
224	223	imaeq2d 5168	. . . . . . . . . . . . . 14
225		ima0 5183	. . . . . . . . . . . . . 14
226	224, 225	syl6eq 2501	. . . . . . . . . . . . 13
227	219, 226	sylan9req 2506	. . . . . . . . . . . 12 $/\$
228		fun 5746	. . . . . . . . . . . 12 $/\$ $/\$
229	113, 227, 228	sylancr 669	. . . . . . . . . . 11 $/\$
230		imaundi 5248	. . . . . . . . . . . . 13
231	64	peano2nnd 10626	. . . . . . . . . . . . . . . . . 18
232	231, 65	syl6eleq 2539	. . . . . . . . . . . . . . . . 17
233	232	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
234		eluzp1p1 11184	. . . . . . . . . . . . . . . . . . 19
235	73, 234	syl 17	. . . . . . . . . . . . . . . . . 18
236	235	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
237	72, 236	eqeltrrd 2530	. . . . . . . . . . . . . . . 16 $/\$
238		fzsplit2 11824	. . . . . . . . . . . . . . . 16 $/\$
239	233, 237, 238	syl2anc 667	. . . . . . . . . . . . . . 15 $/\$
240	239	imaeq2d 5168	. . . . . . . . . . . . . 14 $/\$
241		f1ofo 5821	. . . . . . . . . . . . . . . 16
242		foima 5798	. . . . . . . . . . . . . . . 16
243	215, 241, 242	3syl 18	. . . . . . . . . . . . . . 15
244	243	adantr 467	. . . . . . . . . . . . . 14 $/\$
245	240, 244	eqtr3d 2487	. . . . . . . . . . . . 13 $/\$
246	230, 245	syl5eqr 2499	. . . . . . . . . . . 12 $/\$
247	246	feq2d 5715	. . . . . . . . . . 11 $/\$
248	229, 247	mpbid 214	. . . . . . . . . 10 $/\$
249	248	ffvelrnda 6022	. . . . . . . . 9 $/\$ $/\$
250	110, 249	sseldi 3430	. . . . . . . 8 $/\$ $/\$
251	101, 105, 250	subadd23d 10008	. . . . . . 7 $/\$ $/\$
252		oveq2 6298	. . . . . . . . . 10
253	252	eqeq1d 2453	. . . . . . . . 9
254		oveq2 6298	. . . . . . . . . 10
255	254	eqeq1d 2453	. . . . . . . . 9
256		1m1e0 10678	. . . . . . . . . . . . 13
257		f1ofn 5815	. . . . . . . . . . . . . . . . . . . 20
258	45, 257	syl 17	. . . . . . . . . . . . . . . . . . 19
259	258	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
260		imassrn 5179	. . . . . . . . . . . . . . . . . . . 20
261		f1of 5814	. . . . . . . . . . . . . . . . . . . . . 22
262	213, 261	syl 17	. . . . . . . . . . . . . . . . . . . . 21
263		frn 5735	. . . . . . . . . . . . . . . . . . . . 21
264	262, 263	syl 17	. . . . . . . . . . . . . . . . . . . 20
265	260, 264	syl5ss 3443	. . . . . . . . . . . . . . . . . . 19