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	bilani	\|- ( ( ph /\ t e. V ) -> ( t e. T /\ ( P ` t ) < ( D / 2 ) ) )
55	54	simpld	\|- ( ( ph /\ t e. V ) -> t e. T )
56	52 55	ffvelcdmd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) e. RR )
57	22	adantr	\|- ( ( ph /\ t e. V ) -> ( D / 2 ) e. RR )
58	21	adantr	\|- ( ( ph /\ t e. V ) -> D e. RR )
59	54	simprd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) < ( D / 2 ) )
60		halfpos	\|- ( D e. RR -> ( 0 < D <-> ( D / 2 ) < D ) )
61	21 60	syl	\|- ( ph -> ( 0 < D <-> ( D / 2 ) < D ) )
62	33 61	mpbid	\|- ( ph -> ( D / 2 ) < D )
63	62	adantr	\|- ( ( ph /\ t e. V ) -> ( D / 2 ) < D )
64	56 57 58 59 63	lttrd	\|- ( ( ph /\ t e. V ) -> ( P ` t ) < D )
65	64	adantr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( P ` t ) < D )
66	21	ad2antrr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> D e. RR )
67	56	adantr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( P ` t ) e. RR )
68	19	ad2antrr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
69	55	anim1i	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> ( t e. T /\ -. t e. U ) )
70		eldif	\|- ( t e. ( T \ U ) <-> ( t e. T /\ -. t e. U ) )
71	69 70	sylibr	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> t e. ( T \ U ) )
72		rsp	\|- ( A. t e. ( T \ U ) D <_ ( P ` t ) -> ( t e. ( T \ U ) -> D <_ ( P ` t ) ) )
73	68 71 72	sylc	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> D <_ ( P ` t ) )
74	66 67 73	lensymd	\|- ( ( ( ph /\ t e. V ) /\ -. t e. U ) -> -. ( P ` t ) < D )
75	65 74	condan	\|- ( ( ph /\ t e. V ) -> t e. U )
76	75	ex	\|- ( ph -> ( t e. V -> t e. U ) )
77	2 49 1 76	ssrd	\|- ( ph -> V C_ U )
78		nfv	\|- F/ t e e. RR+
79	2 78	nfan	\|- F/ t ( ph /\ e e. RR+ )
80		nfv	\|- F/ t y e. A
81	79 80	nfan	\|- F/ t ( ( ph /\ e e. RR+ ) /\ y e. A )
82		nfra1	\|- F/ t A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 )
83		nfra1	\|- F/ t A. t e. V ( 1 - e ) < ( y ` t )
84		nfra1	\|- F/ t A. t e. ( T \ U ) ( y ` t ) < e
85	82 83 84	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 )
86	81 85	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 ) )
87		eqid	\|- ( t e. T \|-> ( 1 - ( y ` t ) ) ) = ( t e. T \|-> ( 1 - ( y ` t ) ) )
88		eqid	\|- ( t e. T \|-> 1 ) = ( t e. T \|-> 1 )
89		ssrab2	\|- { t e. T \| ( P ` t ) < ( D / 2 ) } C_ T
90	5 89	eqsstri	\|- V C_ T
91		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 )
92		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 )
93	8	sselda	\|- ( ( ph /\ y e. A ) -> y e. C )
94	4 6 7 93	fcnre	\|- ( ( ph /\ y e. A ) -> y : T --> RR )
95	92 91 94	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 )
96	8	sselda	\|- ( ( ph /\ f e. A ) -> f e. C )
97	4 6 7 96	fcnre	\|- ( ( ph /\ f e. A ) -> f : T --> RR )
98	92 97	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 )
99	92 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 )
100	92 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 )
101	92 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 )
102		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+ )
103		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 ) )
104		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 ) )
105		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 )
106	86 87 88 90 91 95 98 99 100 101 102 103 104 105	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 ) ) )
107	12	adantr	\|- ( ( ph /\ e e. RR+ ) -> D e. RR+ )
108	13	adantr	\|- ( ( ph /\ e e. RR+ ) -> D < 1 )
109	16	adantr	\|- ( ( ph /\ e e. RR+ ) -> P e. A )
110	51	adantr	\|- ( ( ph /\ e e. RR+ ) -> P : T --> RR )
111	17	adantr	\|- ( ( ph /\ e e. RR+ ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
112	19	adantr	\|- ( ( ph /\ e e. RR+ ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
113	97	adantlr	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A ) -> f : T --> RR )
114	9	3adant1r	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
115	10	3adant1r	\|- ( ( ( ph /\ e e. RR+ ) /\ f e. A /\ g e. A ) -> ( t e. T \|-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
116	11	adantlr	\|- ( ( ( ph /\ e e. RR+ ) /\ a e. RR ) -> ( t e. T \|-> a ) e. A )
117		simpr	\|- ( ( ph /\ e e. RR+ ) -> e e. RR+ )
118	3 79 5 107 108 109 110 111 112 113 114 115 116 117	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 ) )
119	106 118	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 ) ) )
120	119	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 ) ) )
121	47 77 120	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 ) ) ) )
122		eleq2	\|- ( v = V -> ( Z e. v <-> Z e. V ) )
123		sseq1	\|- ( v = V -> ( v C_ U <-> V C_ U ) )
124	122 123	anbi12d	\|- ( v = V -> ( ( Z e. v /\ v C_ U ) <-> ( Z e. V /\ V C_ U ) ) )
125		nfcv	\|- F/_ t v
126	125 49	raleqf	\|- ( v = V -> ( A. t e. v ( x ` t ) < e <-> A. t e. V ( x ` t ) < e ) )
127	126	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 ) ) ) )
128	127	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 ) ) ) )
129	128	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 ) ) ) )
130	124 129	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 ) ) ) ) )
131	130	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 ) ) ) )
132	26 121 131	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