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 32023

Description: Lemma for poimir 32037 establishing the vertices of the simplex in poimirlem20 32024. (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 4407	. . . . . . . . . 10
4	3	ifbid 3894	. . . . . . . . 9
5	4	csbeq1d 3356	. . . . . . . 8
6		fveq2 5879	. . . . . . . . . . 11
7	6	fveq2d 5883	. . . . . . . . . 10
8	6	fveq2d 5883	. . . . . . . . . . . . 13
9	8	imaeq1d 5173	. . . . . . . . . . . 12
10	9	xpeq1d 4862	. . . . . . . . . . 11
11	8	imaeq1d 5173	. . . . . . . . . . . 12
12	11	xpeq1d 4862	. . . . . . . . . . 11
13	10, 12	uneq12d 3580	. . . . . . . . . 10
14	7, 13	oveq12d 6326	. . . . . . . . 9
15	14	csbeq2dv 3785	. . . . . . . 8
16	5, 15	eqtrd 2505	. . . . . . 7
17	16	mpteq2dv 4483	. . . . . 6
18	17	eqeq2d 2481	. . . . 5
19		poimirlem22.s	. . . . 5 ..^
20	18, 19	elrab2 3186	. . . 4 ..^ $/\$
21	20	simprbi 471	. . 3
22	1, 21	syl 17	. 2
23		elrabi 3181	. . . . . . . . . . . 12 ..^ ..^
24	23, 19	eleq2s 2567	. . . . . . . . . . 11 ..^
25	1, 24	syl 17	. . . . . . . . . 10 ..^
26		xp1st 6842	. . . . . . . . . 10 ..^ ..^
27	25, 26	syl 17	. . . . . . . . 9 ..^
28		xp1st 6842	. . . . . . . . 9 ..^ ..^
29	27, 28	syl 17	. . . . . . . 8 ..^
30		elmapfn 7512	. . . . . . . 8 ..^
31	29, 30	syl 17	. . . . . . 7
32	31	adantr 472	. . . . . 6 $/\$
33		1ex 9656	. . . . . . . . . 10
34		fnconstg 5784	. . . . . . . . . 10
35	33, 34	ax-mp 5	. . . . . . . . 9
36		c0ex 9655	. . . . . . . . . 10
37		fnconstg 5784	. . . . . . . . . 10
38	36, 37	ax-mp 5	. . . . . . . . 9
39	35, 38	pm3.2i 462	. . . . . . . 8 $/\$
40		xp2nd 6843	. . . . . . . . . . . . 13 ..^
41	27, 40	syl 17	. . . . . . . . . . . 12
42		fvex 5889	. . . . . . . . . . . . 13
43		f1oeq1 5818	. . . . . . . . . . . . 13
44	42, 43	elab 3173	. . . . . . . . . . . 12
45	41, 44	sylib 201	. . . . . . . . . . 11
46		dff1o3 5834	. . . . . . . . . . . 12 $/\$
47	46	simprbi 471	. . . . . . . . . . 11
48	45, 47	syl 17	. . . . . . . . . 10
49		imain 5669	. . . . . . . . . 10
50	48, 49	syl 17	. . . . . . . . 9
51		elfznn0 11913	. . . . . . . . . . . . . 14
52	51	nn0red 10950	. . . . . . . . . . . . 13
53	52	ltp1d 10559	. . . . . . . . . . . 12
54		fzdisj 11852	. . . . . . . . . . . 12
55	53, 54	syl 17	. . . . . . . . . . 11
56	55	imaeq2d 5174	. . . . . . . . . 10
57		ima0 5189	. . . . . . . . . 10
58	56, 57	syl6eq 2521	. . . . . . . . 9
59	50, 58	sylan9req 2526	. . . . . . . 8 $/\$
60		fnun 5692	. . . . . . . 8 $/\$ $/\$
61	39, 59, 60	sylancr 676	. . . . . . 7 $/\$
62		imaundi 5254	. . . . . . . . 9
63		nn0p1nn 10933	. . . . . . . . . . . . . . 15
64	51, 63	syl 17	. . . . . . . . . . . . . 14
65		nnuz 11218	. . . . . . . . . . . . . 14
66	64, 65	syl6eleq 2559	. . . . . . . . . . . . 13
67	66	adantl 473	. . . . . . . . . . . 12 $/\$
68		poimir.0	. . . . . . . . . . . . . . . 16
69	68	nncnd 10647	. . . . . . . . . . . . . . 15
70		npcan1 10065	. . . . . . . . . . . . . . 15
71	69, 70	syl 17	. . . . . . . . . . . . . 14
72	71	adantr 472	. . . . . . . . . . . . 13 $/\$
73		elfzuz3 11823	. . . . . . . . . . . . . . 15
74		peano2uz 11235	. . . . . . . . . . . . . . 15
75	73, 74	syl 17	. . . . . . . . . . . . . 14
76	75	adantl 473	. . . . . . . . . . . . 13 $/\$
77	72, 76	eqeltrrd 2550	. . . . . . . . . . . 12 $/\$
78		fzsplit2 11850	. . . . . . . . . . . 12 $/\$
79	67, 77, 78	syl2anc 673	. . . . . . . . . . 11 $/\$
80	79	imaeq2d 5174	. . . . . . . . . 10 $/\$
81		f1ofo 5835	. . . . . . . . . . . 12
82		foima 5811	. . . . . . . . . . . 12
83	45, 81, 82	3syl 18	. . . . . . . . . . 11
84	83	adantr 472	. . . . . . . . . 10 $/\$
85	80, 84	eqtr3d 2507	. . . . . . . . 9 $/\$
86	62, 85	syl5eqr 2519	. . . . . . . 8 $/\$
87	86	fneq2d 5677	. . . . . . 7 $/\$
88	61, 87	mpbid 215	. . . . . 6 $/\$
89		ovex 6336	. . . . . . 7
90	89	a1i 11	. . . . . 6 $/\$
91		inidm 3632	. . . . . 6
92		eqidd 2472	. . . . . 6 $/\$ $/\$
93		eqidd 2472	. . . . . 6 $/\$ $/\$
94	32, 88, 90, 90, 91, 92, 93	offval 6557	. . . . 5 $/\$
95		elmapi 7511	. . . . . . . . . . . . 13 ..^ ..^
96	29, 95	syl 17	. . . . . . . . . . . 12 ..^
97	96	ffvelrnda 6037	. . . . . . . . . . 11 $/\$ ..^
98		elfzonn0 11988	. . . . . . . . . . 11 ..^
99	97, 98	syl 17	. . . . . . . . . 10 $/\$
100	99	nn0cnd 10951	. . . . . . . . 9 $/\$
101	100	adantlr 729	. . . . . . . 8 $/\$ $/\$
102		ax-1cn 9615	. . . . . . . . . 10
103		0cn 9653	. . . . . . . . . 10
104	102, 103	keepel 3939	. . . . . . . . 9
105	104	a1i 11	. . . . . . . 8 $/\$ $/\$
106		snssi 4107	. . . . . . . . . . 11
107	102, 106	ax-mp 5	. . . . . . . . . 10
108		snssi 4107	. . . . . . . . . . 11
109	103, 108	ax-mp 5	. . . . . . . . . 10
110	107, 109	unssi 3600	. . . . . . . . 9
111	33	fconst 5782	. . . . . . . . . . . . 13
112	36	fconst 5782	. . . . . . . . . . . . 13
113	111, 112	pm3.2i 462	. . . . . . . . . . . 12 $/\$
114		simpr 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$
115	68	nnzd 11062	. . . . . . . . . . . . . . . . . . . . . . 23
116		1z 10991	. . . . . . . . . . . . . . . . . . . . . . . 24
117		peano2z 11002	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
119	115, 118	jctil 546	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
120		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . . . 23
121	120, 116	jctir 547	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
122		fzsubel 11860	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
123	119, 121, 122	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$
124	114, 123	mpbid 215	. . . . . . . . . . . . . . . . . . . 20 $/\$
125	102, 102	pncan3oi 9911	. . . . . . . . . . . . . . . . . . . . 21
126	125	oveq1i 6318	. . . . . . . . . . . . . . . . . . . 20
127	124, 126	syl6eleq 2559	. . . . . . . . . . . . . . . . . . 19 $/\$
128	127	ralrimiva 2809	. . . . . . . . . . . . . . . . . 18
129		simpr 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
130		peano2zm 11004	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	115, 130	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131, 116	jctil 546	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
133		elfzelz 11826	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133, 116	jctir 547	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		fzaddel 11859	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
136	132, 134, 135	syl2an 485	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
137	129, 136	mpbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	71	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . . 22
139	138	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140	137, 139	eleqtrd 2551	. . . . . . . . . . . . . . . . . . . 20 $/\$
141	120	zcnd 11064	. . . . . . . . . . . . . . . . . . . . . . 23
142	133	zcnd 11064	. . . . . . . . . . . . . . . . . . . . . . 23
143		subadd2 9899	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
144	102, 143	mp3an2 1378	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
145		eqcom 2478	. . . . . . . . . . . . . . . . . . . . . . . 24
146		eqcom 2478	. . . . . . . . . . . . . . . . . . . . . . . 24
147	144, 145, 146	3bitr4g 296	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
148	141, 142, 147	syl2anr 486	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
149	148	ralrimiva 2809	. . . . . . . . . . . . . . . . . . . . 21
150	149	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
151		reu6i 3217	. . . . . . . . . . . . . . . . . . . 20 $/\$
152	140, 150, 151	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 $/\$
153	152	ralrimiva 2809	. . . . . . . . . . . . . . . . . 18
154		eqid 2471	. . . . . . . . . . . . . . . . . . 19
155	154	f1ompt 6059	. . . . . . . . . . . . . . . . . 18 $/\$
156	128, 153, 155	sylanbrc 677	. . . . . . . . . . . . . . . . 17
157		f1osng 5867	. . . . . . . . . . . . . . . . . 18 $/\$
158	33, 68, 157	sylancr 676	. . . . . . . . . . . . . . . . 17
159	68	nnred 10646	. . . . . . . . . . . . . . . . . . . . 21
160	159	ltm1d 10561	. . . . . . . . . . . . . . . . . . . 20
161	131	zred 11063	. . . . . . . . . . . . . . . . . . . . 21
162	161, 159	ltnled 9799	. . . . . . . . . . . . . . . . . . . 20
163	160, 162	mpbid 215	. . . . . . . . . . . . . . . . . . 19
164		elfzle2 11829	. . . . . . . . . . . . . . . . . . 19
165	163, 164	nsyl 125	. . . . . . . . . . . . . . . . . 18
166		disjsn 4023	. . . . . . . . . . . . . . . . . 18
167	165, 166	sylibr 217	. . . . . . . . . . . . . . . . 17
168		1re 9660	. . . . . . . . . . . . . . . . . . . . . 22
169	168	ltp1i 10532	. . . . . . . . . . . . . . . . . . . . 21
170	118	zrei 10967	. . . . . . . . . . . . . . . . . . . . . 22
171	168, 170	ltnlei 9773	. . . . . . . . . . . . . . . . . . . . 21
172	169, 171	mpbi 213	. . . . . . . . . . . . . . . . . . . 20
173		elfzle1 11828	. . . . . . . . . . . . . . . . . . . 20
174	172, 173	mto 181	. . . . . . . . . . . . . . . . . . 19
175		disjsn 4023	. . . . . . . . . . . . . . . . . . 19
176	174, 175	mpbir 214	. . . . . . . . . . . . . . . . . 18
177		f1oun 5847	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
178	176, 177	mpanr1 697	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
179	156, 158, 167, 178	syl21anc 1291	. . . . . . . . . . . . . . . 16
180		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . 23
181	174, 180	mtbiri 310	. . . . . . . . . . . . . . . . . . . . . 22
182	181	necon2ai 2672	. . . . . . . . . . . . . . . . . . . . 21
183		ifnefalse 3884	. . . . . . . . . . . . . . . . . . . . 21
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . 20
185	184	mpteq2ia 4478	. . . . . . . . . . . . . . . . . . 19
186	185	uneq1i 3575	. . . . . . . . . . . . . . . . . 18
187	33	a1i 11	. . . . . . . . . . . . . . . . . . 19
188		ssv 3438	. . . . . . . . . . . . . . . . . . . 20
189	188, 68	sseldi 3416	. . . . . . . . . . . . . . . . . . 19
190	68, 65	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . 21
191		fzpred 11870	. . . . . . . . . . . . . . . . . . . . 21
192	190, 191	syl 17	. . . . . . . . . . . . . . . . . . . 20
193		uncom 3569	. . . . . . . . . . . . . . . . . . . 20
194	192, 193	syl6req 2522	. . . . . . . . . . . . . . . . . . 19
195		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20
196	195	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
197	187, 189, 194, 196	fmptapd 6104	. . . . . . . . . . . . . . . . . 18
198	186, 197	syl5eqr 2519	. . . . . . . . . . . . . . . . 17
199	71, 190	eqeltrd 2549	. . . . . . . . . . . . . . . . . . 19
200		uzid 11197	. . . . . . . . . . . . . . . . . . . . 21
201		peano2uz 11235	. . . . . . . . . . . . . . . . . . . . 21
202	131, 200, 201	3syl 18	. . . . . . . . . . . . . . . . . . . 20
203	71, 202	eqeltrrd 2550	. . . . . . . . . . . . . . . . . . 19
204		fzsplit2 11850	. . . . . . . . . . . . . . . . . . 19 $/\$
205	199, 203, 204	syl2anc 673	. . . . . . . . . . . . . . . . . 18
206	71	oveq1d 6323	. . . . . . . . . . . . . . . . . . . 20
207		fzsn 11866	. . . . . . . . . . . . . . . . . . . . 21
208	115, 207	syl 17	. . . . . . . . . . . . . . . . . . . 20
209	206, 208	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19
210	209	uneq2d 3579	. . . . . . . . . . . . . . . . . 18
211	205, 210	eqtr2d 2506	. . . . . . . . . . . . . . . . 17
212	198, 194, 211	f1oeq123d 5824	. . . . . . . . . . . . . . . 16
213	179, 212	mpbid 215	. . . . . . . . . . . . . . 15
214		f1oco 5850	. . . . . . . . . . . . . . 15 $/\$
215	45, 213, 214	syl2anc 673	. . . . . . . . . . . . . 14
216		dff1o3 5834	. . . . . . . . . . . . . . 15 $/\$
217	216	simprbi 471	. . . . . . . . . . . . . 14
218		imain 5669	. . . . . . . . . . . . . 14
219	215, 217, 218	3syl 18	. . . . . . . . . . . . 13
220	64	nnred 10646	. . . . . . . . . . . . . . . . 17
221	220	ltp1d 10559	. . . . . . . . . . . . . . . 16
222		fzdisj 11852	. . . . . . . . . . . . . . . 16
223	221, 222	syl 17	. . . . . . . . . . . . . . 15
224	223	imaeq2d 5174	. . . . . . . . . . . . . 14
225		ima0 5189	. . . . . . . . . . . . . 14
226	224, 225	syl6eq 2521	. . . . . . . . . . . . 13
227	219, 226	sylan9req 2526	. . . . . . . . . . . 12 $/\$
228		fun 5758	. . . . . . . . . . . 12 $/\$ $/\$
229	113, 227, 228	sylancr 676	. . . . . . . . . . 11 $/\$
230		imaundi 5254	. . . . . . . . . . . . 13
231	64	peano2nnd 10648	. . . . . . . . . . . . . . . . . 18
232	231, 65	syl6eleq 2559	. . . . . . . . . . . . . . . . 17
233	232	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
234		eluzp1p1 11208	. . . . . . . . . . . . . . . . . . 19
235	73, 234	syl 17	. . . . . . . . . . . . . . . . . 18
236	235	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
237	72, 236	eqeltrrd 2550	. . . . . . . . . . . . . . . 16 $/\$
238		fzsplit2 11850	. . . . . . . . . . . . . . . 16 $/\$
239	233, 237, 238	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$
240	239	imaeq2d 5174	. . . . . . . . . . . . . 14 $/\$
241		f1ofo 5835	. . . . . . . . . . . . . . . 16
242		foima 5811	. . . . . . . . . . . . . . . 16
243	215, 241, 242	3syl 18	. . . . . . . . . . . . . . 15
244	243	adantr 472	. . . . . . . . . . . . . 14 $/\$
245	240, 244	eqtr3d 2507	. . . . . . . . . . . . 13 $/\$
246	230, 245	syl5eqr 2519	. . . . . . . . . . . 12 $/\$
247	246	feq2d 5725	. . . . . . . . . . 11 $/\$
248	229, 247	mpbid 215	. . . . . . . . . 10 $/\$
249	248	ffvelrnda 6037	. . . . . . . . 9 $/\$ $/\$
250	110, 249	sseldi 3416	. . . . . . . 8 $/\$ $/\$
251	101, 105, 250	subadd23d 10027	. . . . . . 7 $/\$ $/\$
252		oveq2 6316	. . . . . . . . . 10
253	252	eqeq1d 2473	. . . . . . . . 9
254		oveq2 6316	. . . . . . . . . 10
255	254	eqeq1d 2473	. . . . . . . . 9
256		1m1e0 10700	. . . . . . . . . . . . 13
257		f1ofn 5829	. . . . . . . . . . . . . . . . . . . 20
258	45, 257	syl 17	. . . . . . . . . . . . . . . . . . 19
259	258	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
260		imassrn 5185	. . . . . . . . . . . . . . . . . . . 20
261		f1of 5828	. . . . . . . . . . . . . . . . . . . . . 22
262	213, 261	syl 17	. . . . . . . . . . . . . . . . . . . . 21
263		frn 5747	. . . . . . . . . . . . . . . . . . . . 21
264	262, 263	syl 17	. . . . . . . . . . . . . . . . . . . 20
265	260, 264	syl5ss 3429	. . . . . . . . . . . . . . . . . . 19