Metamath Proof Explorer

Theorem stoweid

Description: This theorem proves the Stone-Weierstrass theorem for real-valued functions: let J be a compact topology on T , and C be the set of real continuous functions on T . Assume that A is a subalgebra of C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if r and t are distinct points in T , then there exists a function h in A such that h(r) is distinct from h(t) ). Then, for any continuous function F and for any positive real E , there exists a function f in the subalgebra A , such that f approximates F up to E ( E represents the usual ε value). As a classical example, given any a, b reals, the closed interval T = [ a , b ] could be taken, along with the subalgebra A of real polynomials on T , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [ a , b ] . The proof and lemmas are written following BrosowskiDeutsh p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 stoweid.1 
 |-  F/_ t F
2 stoweid.2 
 |-  F/ t ph
3 stoweid.3 
 |-  K = ( topGen ` ran (,) )
4 stoweid.4 
 |-  ( ph -> J e. Comp )
5 stoweid.5 
 |-  T = U. J
6 stoweid.6 
 |-  C = ( J Cn K )
7 stoweid.7 
 |-  ( ph -> A C_ C )
8 stoweid.8 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
9 stoweid.9 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
10 stoweid.10 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
11 stoweid.11 
 |-  ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. h e. A ( h ` r ) =/= ( h ` t ) )
12 stoweid.12 
 |-  ( ph -> F e. C )
13 stoweid.13 
 |-  ( ph -> E e. RR+ )
14 simpr 
 |-  ( ( ph /\ T = (/) ) -> T = (/) )
15 10 ralrimiva 
 |-  ( ph -> A. x e. RR ( t e. T |-> x ) e. A )
16 1re 
 |-  1 e. RR
17 id 
 |-  ( x = 1 -> x = 1 )
18 17 mpteq2dv 
 |-  ( x = 1 -> ( t e. T |-> x ) = ( t e. T |-> 1 ) )
19 18 eleq1d 
 |-  ( x = 1 -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> 1 ) e. A ) )
20 19 rspccv 
 |-  ( A. x e. RR ( t e. T |-> x ) e. A -> ( 1 e. RR -> ( t e. T |-> 1 ) e. A ) )
21 15 16 20 mpisyl 
 |-  ( ph -> ( t e. T |-> 1 ) e. A )
22 21 adantr 
 |-  ( ( ph /\ T = (/) ) -> ( t e. T |-> 1 ) e. A )
23 14 22 stoweidlem9 
 |-  ( ( ph /\ T = (/) ) -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) )
24 nfv 
 |-  F/ f ph
25 nfv 
 |-  F/ f -. T = (/)
26 24 25 nfan 
 |-  F/ f ( ph /\ -. T = (/) )
27 nfv 
 |-  F/ t -. T = (/)
28 2 27 nfan 
 |-  F/ t ( ph /\ -. T = (/) )
29 eqid 
 |-  ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) ) = ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) )
30 4 adantr 
 |-  ( ( ph /\ -. T = (/) ) -> J e. Comp )
31 7 adantr 
 |-  ( ( ph /\ -. T = (/) ) -> A C_ C )
32 8 3adant1r 
 |-  ( ( ( ph /\ -. T = (/) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
33 9 3adant1r 
 |-  ( ( ( ph /\ -. T = (/) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
34 10 adantlr 
 |-  ( ( ( ph /\ -. T = (/) ) /\ x e. RR ) -> ( t e. T |-> x ) e. A )
35 11 adantlr 
 |-  ( ( ( ph /\ -. T = (/) ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. h e. A ( h ` r ) =/= ( h ` t ) )
36 12 adantr 
 |-  ( ( ph /\ -. T = (/) ) -> F e. C )
37 4re 
 |-  4 e. RR
38 4pos 
 |-  0 < 4
39 37 38 elrpii 
 |-  4 e. RR+
40 39 a1i 
 |-  ( ph -> 4 e. RR+ )
41 40 rpreccld 
 |-  ( ph -> ( 1 / 4 ) e. RR+ )
42 13 41 ifcld 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR+ )
43 42 adantr 
 |-  ( ( ph /\ -. T = (/) ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR+ )
44 neqne 
 |-  ( -. T = (/) -> T =/= (/) )
45 44 adantl 
 |-  ( ( ph /\ -. T = (/) ) -> T =/= (/) )
46 13 rpred 
 |-  ( ph -> E e. RR )
47 4ne0 
 |-  4 =/= 0
48 37 47 rereccli 
 |-  ( 1 / 4 ) e. RR
49 48 a1i 
 |-  ( ph -> ( 1 / 4 ) e. RR )
50 46 49 ifcld 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR )
51 3re 
 |-  3 e. RR
52 3ne0 
 |-  3 =/= 0
53 51 52 rereccli 
 |-  ( 1 / 3 ) e. RR
54 53 a1i 
 |-  ( ph -> ( 1 / 3 ) e. RR )
55 13 rpxrd 
 |-  ( ph -> E e. RR* )
56 41 rpxrd 
 |-  ( ph -> ( 1 / 4 ) e. RR* )
57 xrmin2 
 |-  ( ( E e. RR* /\ ( 1 / 4 ) e. RR* ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ ( 1 / 4 ) )
58 55 56 57 syl2anc 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ ( 1 / 4 ) )
59 3lt4 
 |-  3 < 4
60 3pos 
 |-  0 < 3
61 51 37 60 38 ltrecii 
 |-  ( 3 < 4 <-> ( 1 / 4 ) < ( 1 / 3 ) )
62 59 61 mpbi 
 |-  ( 1 / 4 ) < ( 1 / 3 )
63 62 a1i 
 |-  ( ph -> ( 1 / 4 ) < ( 1 / 3 ) )
64 50 49 54 58 63 lelttrd 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) < ( 1 / 3 ) )
65 64 adantr 
 |-  ( ( ph /\ -. T = (/) ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) < ( 1 / 3 ) )
66 1 26 28 29 3 5 30 6 31 32 33 34 35 36 43 45 65 stoweidlem62 
 |-  ( ( ph /\ -. T = (/) ) -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) )
67 23 66 pm2.61dan 
 |-  ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) )
68 nfv 
 |-  F/ t f e. A
69 2 68 nfan 
 |-  F/ t ( ph /\ f e. A )
70 xrmin1 
 |-  ( ( E e. RR* /\ ( 1 / 4 ) e. RR* ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ E )
71 55 56 70 syl2anc 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ E )
72 71 ad2antrr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ E )
73 7 ad2antrr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> A C_ C )
74 simplr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> f e. A )
75 73 74 sseldd 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> f e. C )
76 3 5 6 75 fcnre 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> f : T --> RR )
77 simpr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> t e. T )
78 76 77 jca 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( f : T --> RR /\ t e. T ) )
79 ffvelrn 
 |-  ( ( f : T --> RR /\ t e. T ) -> ( f ` t ) e. RR )
80 recn 
 |-  ( ( f ` t ) e. RR -> ( f ` t ) e. CC )
81 78 79 80 3syl 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( f ` t ) e. CC )
82 12 ad2antrr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> F e. C )
83 3 5 6 82 fcnre 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> F : T --> RR )
84 83 77 jca 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( F : T --> RR /\ t e. T ) )
85 ffvelrn 
 |-  ( ( F : T --> RR /\ t e. T ) -> ( F ` t ) e. RR )
86 recn 
 |-  ( ( F ` t ) e. RR -> ( F ` t ) e. CC )
87 84 85 86 3syl 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( F ` t ) e. CC )
88 81 87 subcld 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( ( f ` t ) - ( F ` t ) ) e. CC )
89 88 abscld 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( abs ` ( ( f ` t ) - ( F ` t ) ) ) e. RR )
90 16 37 47 3pm3.2i 
 |-  ( 1 e. RR /\ 4 e. RR /\ 4 =/= 0 )
91 redivcl 
 |-  ( ( 1 e. RR /\ 4 e. RR /\ 4 =/= 0 ) -> ( 1 / 4 ) e. RR )
92 90 91 mp1i 
 |-  ( ph -> ( 1 / 4 ) e. RR )
93 46 92 ifcld 
 |-  ( ph -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR )
94 93 ad2antrr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR )
95 46 ad2antrr 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> E e. RR )
96 ltletr 
 |-  ( ( ( abs ` ( ( f ` t ) - ( F ` t ) ) ) e. RR /\ if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) e. RR /\ E e. RR ) -> ( ( ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) /\ if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ E ) -> ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E ) )
97 89 94 95 96 syl3anc 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( ( ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) /\ if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) <_ E ) -> ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E ) )
98 72 97 mpan2d 
 |-  ( ( ( ph /\ f e. A ) /\ t e. T ) -> ( ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) -> ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E ) )
99 69 98 ralimdaa 
 |-  ( ( ph /\ f e. A ) -> ( A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) -> A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E ) )
100 99 reximdva 
 |-  ( ph -> ( E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < if ( E <_ ( 1 / 4 ) , E , ( 1 / 4 ) ) -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E ) )
101 67 100 mpd 
 |-  ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )