Metamath Proof Explorer

Theorem stoweidlem21

Description: Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem21.1 
|- F/_ t G
stoweidlem21.2 
|- F/_ t H
stoweidlem21.3 
|- F/_ t S
stoweidlem21.4 
|- F/ t ph
stoweidlem21.5 
|- G = ( t e. T |-> ( ( H ` t ) + S ) )
stoweidlem21.6 
|- ( ph -> F : T --> RR )
stoweidlem21.7 
|- ( ph -> S e. RR )
stoweidlem21.8 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem21.9 
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem21.10 
|- ( ph -> A. f e. A f : T --> RR )
stoweidlem21.11 
|- ( ph -> H e. A )
stoweidlem21.12 
|- ( ph -> A. t e. T ( abs ` ( ( H ` t ) - ( ( F ` t ) - S ) ) ) < E )
Assertion stoweidlem21 
|- ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )

Proof

Step Hyp Ref Expression
1 stoweidlem21.1 
 |-  F/_ t G
2 stoweidlem21.2 
 |-  F/_ t H
3 stoweidlem21.3 
 |-  F/_ t S
4 stoweidlem21.4 
 |-  F/ t ph
5 stoweidlem21.5 
 |-  G = ( t e. T |-> ( ( H ` t ) + S ) )
6 stoweidlem21.6 
 |-  ( ph -> F : T --> RR )
7 stoweidlem21.7 
 |-  ( ph -> S e. RR )
8 stoweidlem21.8 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9 stoweidlem21.9 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
10 stoweidlem21.10 
 |-  ( ph -> A. f e. A f : T --> RR )
11 stoweidlem21.11 
 |-  ( ph -> H e. A )
12 stoweidlem21.12 
 |-  ( ph -> A. t e. T ( abs ` ( ( H ` t ) - ( ( F ` t ) - S ) ) ) < E )
13 fvconst2g 
 |-  ( ( S e. RR /\ t e. T ) -> ( ( T X. { S } ) ` t ) = S )
14 7 13 sylan 
 |-  ( ( ph /\ t e. T ) -> ( ( T X. { S } ) ` t ) = S )
15 14 eqcomd 
 |-  ( ( ph /\ t e. T ) -> S = ( ( T X. { S } ) ` t ) )
16 15 oveq2d 
 |-  ( ( ph /\ t e. T ) -> ( ( H ` t ) + S ) = ( ( H ` t ) + ( ( T X. { S } ) ` t ) ) )
17 4 16 mpteq2da 
 |-  ( ph -> ( t e. T |-> ( ( H ` t ) + S ) ) = ( t e. T |-> ( ( H ` t ) + ( ( T X. { S } ) ` t ) ) ) )
18 5 17 syl5eq 
 |-  ( ph -> G = ( t e. T |-> ( ( H ` t ) + ( ( T X. { S } ) ` t ) ) ) )
19 fconstmpt 
 |-  ( T X. { S } ) = ( s e. T |-> S )
20 nfcv 
 |-  F/_ s S
21 eqidd 
 |-  ( s = t -> S = S )
22 3 20 21 cbvmpt 
 |-  ( s e. T |-> S ) = ( t e. T |-> S )
23 19 22 eqtri 
 |-  ( T X. { S } ) = ( t e. T |-> S )
24 3 nfeq2 
 |-  F/ t x = S
25 simpl 
 |-  ( ( x = S /\ t e. T ) -> x = S )
26 24 25 mpteq2da 
 |-  ( x = S -> ( t e. T |-> x ) = ( t e. T |-> S ) )
27 26 eleq1d 
 |-  ( x = S -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> S ) e. A ) )
28 27 imbi2d 
 |-  ( x = S -> ( ( ph -> ( t e. T |-> x ) e. A ) <-> ( ph -> ( t e. T |-> S ) e. A ) ) )
29 9 expcom 
 |-  ( x e. RR -> ( ph -> ( t e. T |-> x ) e. A ) )
30 28 29 vtoclga 
 |-  ( S e. RR -> ( ph -> ( t e. T |-> S ) e. A ) )
31 7 30 mpcom 
 |-  ( ph -> ( t e. T |-> S ) e. A )
32 23 31 eqeltrid 
 |-  ( ph -> ( T X. { S } ) e. A )
33 nfcv 
 |-  F/_ t T
34 3 nfsn 
 |-  F/_ t { S }
35 33 34 nfxp 
 |-  F/_ t ( T X. { S } )
36 8 2 35 stoweidlem8 
 |-  ( ( ph /\ H e. A /\ ( T X. { S } ) e. A ) -> ( t e. T |-> ( ( H ` t ) + ( ( T X. { S } ) ` t ) ) ) e. A )
37 11 32 36 mpd3an23 
 |-  ( ph -> ( t e. T |-> ( ( H ` t ) + ( ( T X. { S } ) ` t ) ) ) e. A )
38 18 37 eqeltrd 
 |-  ( ph -> G e. A )
39 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
40 feq1 
 |-  ( f = H -> ( f : T --> RR <-> H : T --> RR ) )
41 40 rspccva 
 |-  ( ( A. f e. A f : T --> RR /\ H e. A ) -> H : T --> RR )
42 10 11 41 syl2anc 
 |-  ( ph -> H : T --> RR )
43 42 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) e. RR )
44 7 adantr 
 |-  ( ( ph /\ t e. T ) -> S e. RR )
45 43 44 readdcld 
 |-  ( ( ph /\ t e. T ) -> ( ( H ` t ) + S ) e. RR )
46 5 fvmpt2 
 |-  ( ( t e. T /\ ( ( H ` t ) + S ) e. RR ) -> ( G ` t ) = ( ( H ` t ) + S ) )
47 39 45 46 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( G ` t ) = ( ( H ` t ) + S ) )
48 47 oveq1d 
 |-  ( ( ph /\ t e. T ) -> ( ( G ` t ) - ( F ` t ) ) = ( ( ( H ` t ) + S ) - ( F ` t ) ) )
49 43 recnd 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) e. CC )
50 6 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
51 50 recnd 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. CC )
52 7 recnd 
 |-  ( ph -> S e. CC )
53 52 adantr 
 |-  ( ( ph /\ t e. T ) -> S e. CC )
54 49 51 53 subsub3d 
 |-  ( ( ph /\ t e. T ) -> ( ( H ` t ) - ( ( F ` t ) - S ) ) = ( ( ( H ` t ) + S ) - ( F ` t ) ) )
55 48 54 eqtr4d 
 |-  ( ( ph /\ t e. T ) -> ( ( G ` t ) - ( F ` t ) ) = ( ( H ` t ) - ( ( F ` t ) - S ) ) )
56 55 fveq2d 
 |-  ( ( ph /\ t e. T ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) = ( abs ` ( ( H ` t ) - ( ( F ` t ) - S ) ) ) )
57 12 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> ( abs ` ( ( H ` t ) - ( ( F ` t ) - S ) ) ) < E )
58 56 57 eqbrtrd 
 |-  ( ( ph /\ t e. T ) -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E )
59 58 ex 
 |-  ( ph -> ( t e. T -> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E ) )
60 4 59 ralrimi 
 |-  ( ph -> A. t e. T ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E )
61 1 nfeq2 
 |-  F/ t f = G
62 fveq1 
 |-  ( f = G -> ( f ` t ) = ( G ` t ) )
63 62 oveq1d 
 |-  ( f = G -> ( ( f ` t ) - ( F ` t ) ) = ( ( G ` t ) - ( F ` t ) ) )
64 63 fveq2d 
 |-  ( f = G -> ( abs ` ( ( f ` t ) - ( F ` t ) ) ) = ( abs ` ( ( G ` t ) - ( F ` t ) ) ) )
65 64 breq1d 
 |-  ( f = G -> ( ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E <-> ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E ) )
66 61 65 ralbid 
 |-  ( f = G -> ( A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E <-> A. t e. T ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E ) )
67 66 rspcev 
 |-  ( ( G e. A /\ A. t e. T ( abs ` ( ( G ` t ) - ( F ` t ) ) ) < E ) -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )
68 38 60 67 syl2anc 
 |-  ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )