stoweidlem52

Description: There exists a neighborhood V as in Lemma 1 of BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem52.1	\|- F/_ t U
	stoweidlem52.2	\|- F/ t ph
	stoweidlem52.3	\|- F/_ t P
	stoweidlem52.4	\|- K = ( topGen ` ran (,) )
	stoweidlem52.5	\|- V = { t e. T \| ( P ` t ) < ( D / 2 ) }
	stoweidlem52.7	\|- T = U. J
	stoweidlem52.8	\|- C = ( J Cn K )
	stoweidlem52.9	\|- ( ph -> A C_ C )
	stoweidlem52.10	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
	stoweidlem52.11	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
	stoweidlem52.12	\|- ( ( ph /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
	stoweidlem52.13	\|- ( ph -> D e. RR+ )
	stoweidlem52.14	\|- ( ph -> D < 1 )
	stoweidlem52.15	\|- ( ph -> U e. J )
	stoweidlem52.16	\|- ( ph -> Z e. U )
	stoweidlem52.17	\|- ( ph -> P e. A )
	stoweidlem52.18	\|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
	stoweidlem52.19	\|- ( ph -> ( P ` Z ) = 0 )
	stoweidlem52.20	\|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
Assertion	stoweidlem52	\|- ( ph -> E. v e. J ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem52.1	\|- F/_ t U
2		stoweidlem52.2	\|- F/ t ph
3		stoweidlem52.3	\|- F/_ t P
4		stoweidlem52.4	\|- K = ( topGen ` ran (,) )
5		stoweidlem52.5	\|- V = { t e. T \| ( P ` t ) < ( D / 2 ) }
6		stoweidlem52.7	\|- T = U. J
7		stoweidlem52.8	\|- C = ( J Cn K )
8		stoweidlem52.9	\|- ( ph -> A C_ C )
9		stoweidlem52.10	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
10		stoweidlem52.11	\|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
11		stoweidlem52.12	\|- ( ( ph /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
12		stoweidlem52.13	\|- ( ph -> D e. RR+ )
13		stoweidlem52.14	\|- ( ph -> D < 1 )
14		stoweidlem52.15	\|- ( ph -> U e. J )
15		stoweidlem52.16	\|- ( ph -> Z e. U )
16		stoweidlem52.17	\|- ( ph -> P e. A )
17		stoweidlem52.18	\|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
18		stoweidlem52.19	\|- ( ph -> ( P ` Z ) = 0 )
19		stoweidlem52.20	\|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
20		nfcv	\|- F/_ t ( D / 2 )
21	12	rpred	\|- ( ph -> D e. RR )
22	21	rehalfcld	\|- ( ph -> ( D / 2 ) e. RR )
23	22	rexrd	\|- ( ph -> ( D / 2 ) e. RR* )
24	8 7	sseqtrdi	\|- ( ph -> A C_ ( J Cn K ) )
25	24 16	sseldd	\|- ( ph -> P e. ( J Cn K ) )
26	20 3 2 4 6 5 23 25	rfcnpre2	\|- ( ph -> V e. J )
27		elssuni	\|- ( U e. J -> U C_ U. J )
28	14 27	syl	\|- ( ph -> U C_ U. J )
29	28 6	sseqtrrdi	\|- ( ph -> U C_ T )
30	29 15	sseldd	\|- ( ph -> Z e. T )
31		2re	\|- 2 e. RR
32	31	a1i	\|- ( ph -> 2 e. RR )
33	12	rpgt0d	\|- ( ph -> 0 < D )
34		2pos	\|- 0 < 2
35	34	a1i	\|- ( ph -> 0 < 2 )
36	21 32 33 35	divgt0d	\|- ( ph -> 0 < ( D / 2 ) )
37	18 36	eqbrtrd	\|- ( ph -> ( P ` Z ) < ( D / 2 ) )
38		nfcv	\|- F/_ t Z
39		nfcv	\|- F/_ t T
40	3 38	nffv	\|- F/_ t ( P ` Z )
41		nfcv	\|- F/_ t <
42	40 41 20	nfbr	\|- F/ t ( P ` Z ) < ( D / 2 )
43		fveq2	\|- ( t = Z -> ( P ` t ) = ( P ` Z ) )
44	43	breq1d	\|- ( t = Z -> ( ( P ` t ) < ( D / 2 ) <-> ( P ` Z ) < ( D / 2 ) ) )
45	38 39 42 44	elrabf	\|- ( Z e. { t e. T \| ( P ` t ) < ( D / 2 ) } <-> ( Z e. T /\ ( P ` Z ) < ( D / 2 ) ) )
46	30 37 45	sylanbrc	\|- ( ph -> Z e. { t e. T \| ( P ` t ) < ( D / 2 ) } )
47	46 5	eleqtrrdi	\|- ( ph -> Z e. V )
48		nfrab1	\|- F/_ t { t e. T \| ( P ` t ) < ( D / 2 ) }
49	5 48	nfcxfr	\|- F/_ t V
50	8 16	sseldd	\|- ( ph -> P e. C )
51	4 6 7 50	fcnre	\|- ( ph -> P : T --> RR )
52	51	adantr	\|- ( ( ph /\ t e. V ) -> P : T --> RR )
53	5	reqabi	\|- ( t e. V <-> ( t e. T /\ ( P ` t ) < ( D / 2 ) ) )
54	53	biimpi	\|- ( t e. V -> ( t e. T /\ ( P ` t ) < ( D / 2 ) ) )
55	54	adantl	\|- ( ( ph /\ t e. V ) -> ( t e. T /\ ( P ` t ) < ( D / 2 ) ) )
56	55	simpld	\|- ( ( ph /\ t e. V ) -> t e. T )
57	52 56	ffvelcdmd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) e. RR )
58	22	adantr	\|- ( ( ph /\ t e. V ) -> ( D / 2 ) e. RR )
59	21	adantr	\|- ( ( ph /\ t e. V ) -> D e. RR )
60	55	simprd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) < ( D / 2 ) )
61		halfpos	\|- ( D e. RR -> ( 0 < D <-> ( D / 2 ) < D ) )
62	21 61	syl	\|- ( ph -> ( 0 < D <-> ( D / 2 ) < D ) )
63	33 62	mpbid	\|- ( ph -> ( D / 2 ) < D )
64	63	adantr	\|- ( ( ph /\ t e. V ) -> ( D / 2 ) < D )
65	57 58 59 60 64	lttrd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) < D )
66	65	adantr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( P ` t ) < D )
67	21	ad2antrr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> D e. RR )
68	57	adantr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( P ` t ) e. RR )
69	19	ad2antrr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
70	56	anim1i	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( t e. T /\ -. t e. U ) )
71		eldif	\|- ( t e. ( T \ U ) <-> ( t e. T /\ -. t e. U ) )
72	70 71	sylibr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> t e. ( T \ U ) )
73		rsp	\|- ( A. t e. ( T \ U ) D <_ ( P ` t ) -> ( t e. ( T \ U ) -> D <_ ( P ` t ) ) )
74	69 72 73	sylc	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> D <_ ( P ` t ) )
75	67 68 74	lensymd	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> -. ( P ` t ) < D )
76	66 75	condan	\|- ( ( ph /\ t e. V ) -> t e. U )
77	76	ex	\|- ( ph -> ( t e. V -> t e. U ) )
78	2 49 1 77	ssrd	\|- ( ph -> V C_ U )
79		nfv	\|- F/ t e e. RR+
80	2 79	nfan	\|- F/ t ( ph /\ e e. RR+ )
81		nfv	\|- F/ t y e. A
82	80 81	nfan	\|- F/ t ( ( ph /\ e e. RR+ ) /\ y e. A )
83		nfra1	\|- F/ t A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 )
84		nfra1	\|- F/ t A. t e. V ( 1 - e ) < ( y ` t )
85		nfra1	\|- F/ t A. t e. ( T \ U ) ( y ` t ) < e
86	83 84 85	nf3an	\|- F/ t ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e )
87	82 86	nfan	\|- F/ t ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) )
88		eqid	\|- ( t e. T \|-> ( 1 - ( y ` t ) ) ) = ( t e. T \|-> ( 1 - ( y ` t ) ) )
89		eqid	\|- ( t e. T \|-> 1 ) = ( t e. T \|-> 1 )
90		ssrab2	\|- { t e. T \| ( P ` t ) < ( D / 2 ) } C_ T
91	5 90	eqsstri	\|- V C_ T
92		simplr	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> y e. A )
93		simplll	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> ph )
94	8	sselda	\|- ( ( ph /\ y e. A ) -> y e. C )
95	4 6 7 94	fcnre	\|- ( ( ph /\ y e. A ) -> y : T --> RR )
96	93 92 95	syl2anc	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> y : T --> RR )
97	8	sselda	\|- ( ( ph /\ f e. A ) -> f e. C )
98	4 6 7 97	fcnre	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
99	93 98	sylan	\|- ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) /\ f e. A ) -> f : T --> RR )
100	93 9	syl3an1	\|- ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
101	93 10	syl3an1	\|- ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
102	93 11	sylan	\|- ( ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
103		simpllr	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> e e. RR+ )
104		simpr1	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) )
105		simpr2	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> A. t e. V ( 1 - e ) < ( y ` t ) )
106		simpr3	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> A. t e. ( T \ U ) ( y ` t ) < e )
107	87 88 89 91 92 96 99 100 101 102 103 104 105 106	stoweidlem41	\|- ( ( ( ( ph /\ e e. RR+ ) /\ y e. A ) /\ ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) ) -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) )
108	12	adantr	\|- ( ( ph /\ e e. RR+ ) -> D e. RR+ )
109	13	adantr	\|- ( ( ph /\ e e. RR+ ) -> D < 1 )
110	16	adantr	\|- ( ( ph /\ e e. RR+ ) -> P e. A )
111	51	adantr	\|- ( ( ph /\ e e. RR+ ) -> P : T --> RR )
112	17	adantr	\|- ( ( ph /\ e e. RR+ ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
113	19	adantr	\|- ( ( ph /\ e e. RR+ ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
114	98	adantlr	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A ) -> f : T --> RR )
115	9	3adant1r	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
116	10	3adant1r	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
117	11	adantlr	\|- ( ( ( ph /\ e e. RR+ ) /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
118		simpr	\|- ( ( ph /\ e e. RR+ ) -> e e. RR+ )
119	3 80 5 108 109 110 111 112 113 114 115 116 117 118	stoweidlem49	\|- ( ( ph /\ e e. RR+ ) -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - e ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < e ) )
120	107 119	r19.29a	\|- ( ( ph /\ e e. RR+ ) -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) )
121	120	ralrimiva	\|- ( ph -> A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) )
122	47 78 121	jca31	\|- ( ph -> ( ( Z e. V /\ V C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
123		eleq2	\|- ( v = V -> ( Z e. v <-> Z e. V ) )
124		sseq1	\|- ( v = V -> ( v C_ U <-> V C_ U ) )
125	123 124	anbi12d	\|- ( v = V -> ( ( Z e. v /\ v C_ U ) <-> ( Z e. V /\ V C_ U ) ) )
126		nfcv	\|- F/_ t v
127	126 49	raleqf	\|- ( v = V -> ( A. t e. v ( x ` t ) < e <-> A. t e. V ( x ` t ) < e ) )
128	127	3anbi2d	\|- ( v = V -> ( ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) <-> ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
129	128	rexbidv	\|- ( v = V -> ( E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) <-> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
130	129	ralbidv	\|- ( v = V -> ( A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) <-> A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
131	125 130	anbi12d	\|- ( v = V -> ( ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) <-> ( ( Z e. V /\ V C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) ) )
132	131	rspcev	\|- ( ( V e. J /\ ( ( Z e. V /\ V C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) ) -> E. v e. J ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
133	26 122 132	syl2anc	\|- ( ph -> E. v e. J ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )

Metamath Proof Explorer

Theorem stoweidlem52

Proof