Metamath Proof Explorer

Theorem stoweidlem61

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 92: g is in the subalgebra, and for all t in T , abs( f(t) - g(t) ) < 2*ε. Here F is used to represent f in the paper, and E is used to represent ε. For this lemma there's the further assumption that the function F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem61.1 
|- F/_ t F
stoweidlem61.2 
|- F/ t ph
stoweidlem61.3 
|- K = ( topGen ` ran (,) )
stoweidlem61.4 
|- ( ph -> J e. Comp )
stoweidlem61.5 
|- T = U. J
stoweidlem61.6 
|- ( ph -> T =/= (/) )
stoweidlem61.7 
|- C = ( J Cn K )
stoweidlem61.8 
|- ( ph -> A C_ C )
stoweidlem61.9 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem61.10 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem61.11 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem61.12 
|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
stoweidlem61.13 
|- ( ph -> F e. C )
stoweidlem61.14 
|- ( ph -> A. t e. T 0 <_ ( F ` t ) )
stoweidlem61.15 
|- ( ph -> E e. RR+ )
stoweidlem61.16 
|- ( ph -> E < ( 1 / 3 ) )
Assertion stoweidlem61 
|- ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) )

Proof

Step Hyp Ref Expression
1 stoweidlem61.1 
 |-  F/_ t F
2 stoweidlem61.2 
 |-  F/ t ph
3 stoweidlem61.3 
 |-  K = ( topGen ` ran (,) )
4 stoweidlem61.4 
 |-  ( ph -> J e. Comp )
5 stoweidlem61.5 
 |-  T = U. J
6 stoweidlem61.6 
 |-  ( ph -> T =/= (/) )
7 stoweidlem61.7 
 |-  C = ( J Cn K )
8 stoweidlem61.8 
 |-  ( ph -> A C_ C )
9 stoweidlem61.9 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
10 stoweidlem61.10 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
11 stoweidlem61.11 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
12 stoweidlem61.12 
 |-  ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
13 stoweidlem61.13 
 |-  ( ph -> F e. C )
14 stoweidlem61.14 
 |-  ( ph -> A. t e. T 0 <_ ( F ` t ) )
15 stoweidlem61.15 
 |-  ( ph -> E e. RR+ )
16 stoweidlem61.16 
 |-  ( ph -> E < ( 1 / 3 ) )
17 eqid 
 |-  ( j e. ( 0 ... n ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } ) = ( j e. ( 0 ... n ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
18 eqid 
 |-  ( j e. ( 0 ... n ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) = ( j e. ( 0 ... n ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
19 1 2 3 5 7 17 18 4 6 8 9 10 11 12 13 14 15 16 stoweidlem60 
 |-  ( ph -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
20 nfv 
 |-  F/ t g e. A
21 2 20 nfan 
 |-  F/ t ( ph /\ g e. A )
22 15 ad2antrr 
 |-  ( ( ( ph /\ g e. A ) /\ t e. T ) -> E e. RR+ )
23 3 5 7 13 fcnre 
 |-  ( ph -> F : T --> RR )
24 23 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
25 24 adantlr 
 |-  ( ( ( ph /\ g e. A ) /\ t e. T ) -> ( F ` t ) e. RR )
26 8 sselda 
 |-  ( ( ph /\ g e. A ) -> g e. C )
27 3 5 7 26 fcnre 
 |-  ( ( ph /\ g e. A ) -> g : T --> RR )
28 27 ffvelrnda 
 |-  ( ( ( ph /\ g e. A ) /\ t e. T ) -> ( g ` t ) e. RR )
29 simpll1 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> E e. RR+ )
30 simpll2 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( F ` t ) e. RR )
31 simpll3 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( g ` t ) e. RR )
32 simplr 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> j e. RR )
33 simprll 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) )
34 simprlr 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
35 simprrr 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) )
36 simprrl 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) )
37 29 30 31 32 33 34 35 36 stoweidlem13 
 |-  ( ( ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) /\ j e. RR ) /\ ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) ) -> ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) )
38 37 rexlimdva2 
 |-  ( ( E e. RR+ /\ ( F ` t ) e. RR /\ ( g ` t ) e. RR ) -> ( E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) ) )
39 22 25 28 38 syl3anc 
 |-  ( ( ( ph /\ g e. A ) /\ t e. T ) -> ( E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) ) )
40 21 39 ralimdaa 
 |-  ( ( ph /\ g e. A ) -> ( A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) ) )
41 40 reximdva 
 |-  ( ph -> ( E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) ) )
42 19 41 mpd 
 |-  ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) )