Metamath Proof Explorer

Theorem stoweidlem62

Description: This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows BrosowskiDeutsh p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017) (Revised by AV, 13-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 stoweidlem62.1 
 |-  F/_ t F
2 stoweidlem62.2 
 |-  F/ f ph
3 stoweidlem62.3 
 |-  F/ t ph
4 stoweidlem62.4 
 |-  H = ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) )
5 stoweidlem62.5 
 |-  K = ( topGen ` ran (,) )
6 stoweidlem62.6 
 |-  T = U. J
7 stoweidlem62.7 
 |-  ( ph -> J e. Comp )
8 stoweidlem62.8 
 |-  C = ( J Cn K )
9 stoweidlem62.9 
 |-  ( ph -> A C_ C )
10 stoweidlem62.10 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
11 stoweidlem62.11 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
12 stoweidlem62.12 
 |-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
13 stoweidlem62.13 
 |-  ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
14 stoweidlem62.14 
 |-  ( ph -> F e. C )
15 stoweidlem62.15 
 |-  ( ph -> E e. RR+ )
16 stoweidlem62.16 
 |-  ( ph -> T =/= (/) )
17 stoweidlem62.17 
 |-  ( ph -> E < ( 1 / 3 ) )
18 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) )
19 4 18 nfcxfr 
 |-  F/_ t H
20 eleq1w 
 |-  ( g = h -> ( g e. A <-> h e. A ) )
21 20 3anbi3d 
 |-  ( g = h -> ( ( ph /\ f e. A /\ g e. A ) <-> ( ph /\ f e. A /\ h e. A ) ) )
22 fveq1 
 |-  ( g = h -> ( g ` t ) = ( h ` t ) )
23 22 oveq2d 
 |-  ( g = h -> ( ( f ` t ) + ( g ` t ) ) = ( ( f ` t ) + ( h ` t ) ) )
24 23 mpteq2dv 
 |-  ( g = h -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) = ( t e. T |-> ( ( f ` t ) + ( h ` t ) ) ) )
25 24 eleq1d 
 |-  ( g = h -> ( ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( f ` t ) + ( h ` t ) ) ) e. A ) )
26 21 25 imbi12d 
 |-  ( g = h -> ( ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A ) <-> ( ( ph /\ f e. A /\ h e. A ) -> ( t e. T |-> ( ( f ` t ) + ( h ` t ) ) ) e. A ) ) )
27 26 10 chvarvv 
 |-  ( ( ph /\ f e. A /\ h e. A ) -> ( t e. T |-> ( ( f ` t ) + ( h ` t ) ) ) e. A )
28 22 oveq2d 
 |-  ( g = h -> ( ( f ` t ) x. ( g ` t ) ) = ( ( f ` t ) x. ( h ` t ) ) )
29 28 mpteq2dv 
 |-  ( g = h -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( f ` t ) x. ( h ` t ) ) ) )
30 29 eleq1d 
 |-  ( g = h -> ( ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A <-> ( t e. T |-> ( ( f ` t ) x. ( h ` t ) ) ) e. A ) )
31 21 30 imbi12d 
 |-  ( g = h -> ( ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) <-> ( ( ph /\ f e. A /\ h e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( h ` t ) ) ) e. A ) ) )
32 31 11 chvarvv 
 |-  ( ( ph /\ f e. A /\ h e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( h ` t ) ) ) e. A )
33 1 nfrn 
 |-  F/_ t ran F
34 nfcv 
 |-  F/_ t RR
35 nfcv 
 |-  F/_ t <
36 33 34 35 nfinf 
 |-  F/_ t inf ( ran F , RR , < )
37 eqid 
 |-  ( T X. { -u inf ( ran F , RR , < ) } ) = ( T X. { -u inf ( ran F , RR , < ) } )
38 cmptop 
 |-  ( J e. Comp -> J e. Top )
39 7 38 syl 
 |-  ( ph -> J e. Top )
40 14 8 eleqtrdi 
 |-  ( ph -> F e. ( J Cn K ) )
41 1 3 6 5 7 40 16 stoweidlem29 
 |-  ( ph -> ( inf ( ran F , RR , < ) e. ran F /\ inf ( ran F , RR , < ) e. RR /\ A. t e. T inf ( ran F , RR , < ) <_ ( F ` t ) ) )
42 41 simp2d 
 |-  ( ph -> inf ( ran F , RR , < ) e. RR )
43 1 36 3 6 37 5 39 8 14 42 stoweidlem47 
 |-  ( ph -> ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) ) e. C )
44 4 43 eqeltrid 
 |-  ( ph -> H e. C )
45 41 simp3d 
 |-  ( ph -> A. t e. T inf ( ran F , RR , < ) <_ ( F ` t ) )
46 45 r19.21bi 
 |-  ( ( ph /\ t e. T ) -> inf ( ran F , RR , < ) <_ ( F ` t ) )
47 5 6 8 14 fcnre 
 |-  ( ph -> F : T --> RR )
48 47 ffvelrnda 
 |-  ( ( ph /\ t e. T ) -> ( F ` t ) e. RR )
49 42 adantr 
 |-  ( ( ph /\ t e. T ) -> inf ( ran F , RR , < ) e. RR )
50 48 49 subge0d 
 |-  ( ( ph /\ t e. T ) -> ( 0 <_ ( ( F ` t ) - inf ( ran F , RR , < ) ) <-> inf ( ran F , RR , < ) <_ ( F ` t ) ) )
51 46 50 mpbird 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( ( F ` t ) - inf ( ran F , RR , < ) ) )
52 simpr 
 |-  ( ( ph /\ t e. T ) -> t e. T )
53 48 49 resubcld 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) - inf ( ran F , RR , < ) ) e. RR )
54 4 fvmpt2 
 |-  ( ( t e. T /\ ( ( F ` t ) - inf ( ran F , RR , < ) ) e. RR ) -> ( H ` t ) = ( ( F ` t ) - inf ( ran F , RR , < ) ) )
55 52 53 54 syl2anc 
 |-  ( ( ph /\ t e. T ) -> ( H ` t ) = ( ( F ` t ) - inf ( ran F , RR , < ) ) )
56 51 55 breqtrrd 
 |-  ( ( ph /\ t e. T ) -> 0 <_ ( H ` t ) )
57 56 ex 
 |-  ( ph -> ( t e. T -> 0 <_ ( H ` t ) ) )
58 3 57 ralrimi 
 |-  ( ph -> A. t e. T 0 <_ ( H ` t ) )
59 15 rphalfcld 
 |-  ( ph -> ( E / 2 ) e. RR+ )
60 15 rpred 
 |-  ( ph -> E e. RR )
61 60 rehalfcld 
 |-  ( ph -> ( E / 2 ) e. RR )
62 3re 
 |-  3 e. RR
63 3ne0 
 |-  3 =/= 0
64 62 63 rereccli 
 |-  ( 1 / 3 ) e. RR
65 64 a1i 
 |-  ( ph -> ( 1 / 3 ) e. RR )
66 rphalflt 
 |-  ( E e. RR+ -> ( E / 2 ) < E )
67 15 66 syl 
 |-  ( ph -> ( E / 2 ) < E )
68 61 60 65 67 17 lttrd 
 |-  ( ph -> ( E / 2 ) < ( 1 / 3 ) )
69 19 3 5 7 6 16 8 9 27 32 12 13 44 58 59 68 stoweidlem61 
 |-  ( ph -> E. h e. A A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) )
70 nfra1 
 |-  F/ t A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) )
71 3 70 nfan 
 |-  F/ t ( ph /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) )
72 rsp 
 |-  ( A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) -> ( t e. T -> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) ) )
73 15 rpcnd 
 |-  ( ph -> E e. CC )
74 2cnd 
 |-  ( ph -> 2 e. CC )
75 2ne0 
 |-  2 =/= 0
76 75 a1i 
 |-  ( ph -> 2 =/= 0 )
77 73 74 76 divcan2d 
 |-  ( ph -> ( 2 x. ( E / 2 ) ) = E )
78 77 breq2d 
 |-  ( ph -> ( ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) <-> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
79 78 biimpd 
 |-  ( ph -> ( ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) -> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
80 72 79 sylan9r 
 |-  ( ( ph /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) ) -> ( t e. T -> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
81 71 80 ralrimi 
 |-  ( ( ph /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) ) -> A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
82 81 ex 
 |-  ( ph -> ( A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) -> A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
83 82 reximdv 
 |-  ( ph -> ( E. h e. A A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < ( 2 x. ( E / 2 ) ) -> E. h e. A A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
84 69 83 mpd 
 |-  ( ph -> E. h e. A A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
85 nfmpt1 
 |-  F/_ t ( t e. T |-> ( ( h ` t ) + inf ( ran F , RR , < ) ) )
86 nfcv 
 |-  F/_ t h
87 nfv 
 |-  F/ t h e. A
88 nfra1 
 |-  F/ t A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E
89 87 88 nfan 
 |-  F/ t ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
90 3 89 nfan 
 |-  F/ t ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) )
91 eqid 
 |-  ( t e. T |-> ( ( h ` t ) + inf ( ran F , RR , < ) ) ) = ( t e. T |-> ( ( h ` t ) + inf ( ran F , RR , < ) ) )
92 47 adantr 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> F : T --> RR )
93 42 adantr 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> inf ( ran F , RR , < ) e. RR )
94 10 3adant1r 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
95 12 adantlr 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ x e. RR ) -> ( t e. T |-> x ) e. A )
96 9 sseld 
 |-  ( ph -> ( f e. A -> f e. C ) )
97 8 eleq2i 
 |-  ( f e. C <-> f e. ( J Cn K ) )
98 96 97 syl6ib 
 |-  ( ph -> ( f e. A -> f e. ( J Cn K ) ) )
99 eqid 
 |-  U. J = U. J
100 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
101 5 unieqi 
 |-  U. K = U. ( topGen ` ran (,) )
102 100 101 eqtr4i 
 |-  RR = U. K
103 99 102 cnf 
 |-  ( f e. ( J Cn K ) -> f : U. J --> RR )
104 98 103 syl6 
 |-  ( ph -> ( f e. A -> f : U. J --> RR ) )
105 feq2 
 |-  ( T = U. J -> ( f : T --> RR <-> f : U. J --> RR ) )
106 6 105 mp1i 
 |-  ( ph -> ( f : T --> RR <-> f : U. J --> RR ) )
107 104 106 sylibrd 
 |-  ( ph -> ( f e. A -> f : T --> RR ) )
108 2 107 ralrimi 
 |-  ( ph -> A. f e. A f : T --> RR )
109 108 adantr 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> A. f e. A f : T --> RR )
110 simprl 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> h e. A )
111 55 eqcomd 
 |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) - inf ( ran F , RR , < ) ) = ( H ` t ) )
112 111 oveq2d 
 |-  ( ( ph /\ t e. T ) -> ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) = ( ( h ` t ) - ( H ` t ) ) )
113 112 fveq2d 
 |-  ( ( ph /\ t e. T ) -> ( abs ` ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) ) = ( abs ` ( ( h ` t ) - ( H ` t ) ) ) )
114 113 adantlr 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ t e. T ) -> ( abs ` ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) ) = ( abs ` ( ( h ` t ) - ( H ` t ) ) ) )
115 simplrr 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ t e. T ) -> A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
116 rspa 
 |-  ( ( A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E /\ t e. T ) -> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
117 115 116 sylancom 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ t e. T ) -> ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E )
118 114 117 eqbrtrd 
 |-  ( ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) /\ t e. T ) -> ( abs ` ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) ) < E )
119 118 ex 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> ( t e. T -> ( abs ` ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) ) < E ) )
120 90 119 ralrimi 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> A. t e. T ( abs ` ( ( h ` t ) - ( ( F ` t ) - inf ( ran F , RR , < ) ) ) ) < E )
121 85 86 36 90 91 92 93 94 95 109 110 120 stoweidlem21 
 |-  ( ( ph /\ ( h e. A /\ A. t e. T ( abs ` ( ( h ` t ) - ( H ` t ) ) ) < E ) ) -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )
122 84 121 rexlimddv 
 |-  ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )