Metamath Proof Explorer

Theorem stoweidlem54

Description: There exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem54.1 
|- F/ i ph
stoweidlem54.2 
|- F/ t ph
stoweidlem54.3 
|- F/ y ph
stoweidlem54.4 
|- F/ w ph
stoweidlem54.5 
|- T = U. J
stoweidlem54.6 
|- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
stoweidlem54.7 
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
stoweidlem54.8 
|- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( y ` i ) ` t ) ) )
stoweidlem54.9 
|- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
stoweidlem54.10 
|- V = { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }
stoweidlem54.11 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem54.12 
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem54.13 
|- ( ph -> M e. NN )
stoweidlem54.14 
|- ( ph -> W : ( 1 ... M ) --> V )
stoweidlem54.15 
|- ( ph -> B C_ T )
stoweidlem54.16 
|- ( ph -> D C_ U. ran W )
stoweidlem54.17 
|- ( ph -> D C_ T )
stoweidlem54.18 
|- ( ph -> E. y ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )
stoweidlem54.19 
|- ( ph -> T e. _V )
stoweidlem54.20 
|- ( ph -> E e. RR+ )
stoweidlem54.21 
|- ( ph -> E < ( 1 / 3 ) )
Assertion stoweidlem54 
|- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem54.1 
 |-  F/ i ph
2 stoweidlem54.2 
 |-  F/ t ph
3 stoweidlem54.3 
 |-  F/ y ph
4 stoweidlem54.4 
 |-  F/ w ph
5 stoweidlem54.5 
 |-  T = U. J
6 stoweidlem54.6 
 |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
7 stoweidlem54.7 
 |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )
8 stoweidlem54.8 
 |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( y ` i ) ` t ) ) )
9 stoweidlem54.9 
 |-  Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )
10 stoweidlem54.10 
 |-  V = { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }
11 stoweidlem54.11 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
12 stoweidlem54.12 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
13 stoweidlem54.13 
 |-  ( ph -> M e. NN )
14 stoweidlem54.14 
 |-  ( ph -> W : ( 1 ... M ) --> V )
15 stoweidlem54.15 
 |-  ( ph -> B C_ T )
16 stoweidlem54.16 
 |-  ( ph -> D C_ U. ran W )
17 stoweidlem54.17 
 |-  ( ph -> D C_ T )
18 stoweidlem54.18 
 |-  ( ph -> E. y ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )
19 stoweidlem54.19 
 |-  ( ph -> T e. _V )
20 stoweidlem54.20 
 |-  ( ph -> E e. RR+ )
21 stoweidlem54.21 
 |-  ( ph -> E < ( 1 / 3 ) )
22 nfv 
 |-  F/ y E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )
23 nfv 
 |-  F/ i y : ( 1 ... M ) --> Y
24 nfra1 
 |-  F/ i A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
25 23 24 nfan 
 |-  F/ i ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) )
26 1 25 nfan 
 |-  F/ i ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )
27 nfcv 
 |-  F/_ t y
28 nfcv 
 |-  F/_ t ( 1 ... M )
29 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
30 nfcv 
 |-  F/_ t A
31 29 30 nfrabw 
 |-  F/_ t { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
32 6 31 nfcxfr 
 |-  F/_ t Y
33 27 28 32 nff 
 |-  F/ t y : ( 1 ... M ) --> Y
34 nfra1 
 |-  F/ t A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M )
35 nfra1 
 |-  F/ t A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t )
36 34 35 nfan 
 |-  F/ t ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
37 28 36 nfralw 
 |-  F/ t A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
38 33 37 nfan 
 |-  F/ t ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) )
39 2 38 nfan 
 |-  F/ t ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )
40 nfv 
 |-  F/ w ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) )
41 4 40 nfan 
 |-  F/ w ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )
42 nfrab1 
 |-  F/_ w { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }
43 10 42 nfcxfr 
 |-  F/_ w V
44 eqid 
 |-  ( seq 1 ( P , y ) ` M ) = ( seq 1 ( P , y ) ` M )
45 13 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> M e. NN )
46 14 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> W : ( 1 ... M ) --> V )
47 simprl 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> y : ( 1 ... M ) --> Y )
48 simpr 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ w e. V ) -> w e. V )
49 10 rabeq2i 
 |-  ( w e. V <-> ( w e. J /\ A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) ) )
50 49 simplbi 
 |-  ( w e. V -> w e. J )
51 elssuni 
 |-  ( w e. J -> w C_ U. J )
52 51 5 sseqtrrdi 
 |-  ( w e. J -> w C_ T )
53 48 50 52 3syl 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ w e. V ) -> w C_ T )
54 16 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> D C_ U. ran W )
55 17 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> D C_ T )
56 15 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> B C_ T )
57 r19.26 
 |-  ( A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) <-> ( A. i e. ( 1 ... M ) A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. i e. ( 1 ... M ) A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) )
58 57 simplbi 
 |-  ( A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) -> A. i e. ( 1 ... M ) A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) )
59 58 ad2antll 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> A. i e. ( 1 ... M ) A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) )
60 59 r19.21bi 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) )
61 57 simprbi 
 |-  ( A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) -> A. i e. ( 1 ... M ) A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
62 61 ad2antll 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> A. i e. ( 1 ... M ) A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
63 62 r19.21bi 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) )
64 11 3adant1r 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
65 12 adantlr 
 |-  ( ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) /\ f e. A ) -> f : T --> RR )
66 19 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> T e. _V )
67 20 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> E e. RR+ )
68 21 adantr 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> E < ( 1 / 3 ) )
69 26 39 41 43 6 7 44 8 9 45 46 47 53 54 55 56 60 63 64 65 66 67 68 stoweidlem51 
 |-  ( ( ph /\ ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) ) -> E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) ) )
70 3 22 18 69 exlimdd 
 |-  ( ph -> E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) ) )
71 df-rex 
 |-  ( E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) <-> E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) ) )
72 70 71 sylibr 
 |-  ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )