Metamath Proof Explorer

Theorem stoweidlem39

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that r is a finite subset of W , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here D is used to represent A in the paper's Lemma 2 (because A is used for the subalgebra), M is used to represent m in the paper, E is used to represent ε, and v_i is used to represent V(t_i). W is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem39.1 
|- F/ h ph
stoweidlem39.2 
|- F/ t ph
stoweidlem39.3 
|- F/ w ph
stoweidlem39.4 
|- U = ( T \ B )
stoweidlem39.5 
|- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
stoweidlem39.6 
|- 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 ) ) }
stoweidlem39.7 
|- ( ph -> r e. ( ~P W i^i Fin ) )
stoweidlem39.8 
|- ( ph -> D C_ U. r )
stoweidlem39.9 
|- ( ph -> D =/= (/) )
stoweidlem39.10 
|- ( ph -> E e. RR+ )
stoweidlem39.11 
|- ( ph -> B C_ T )
stoweidlem39.12 
|- ( ph -> W e. _V )
stoweidlem39.13 
|- ( ph -> A e. _V )
Assertion stoweidlem39 
|- ( ph -> E. m e. NN E. v ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem39.1 
 |-  F/ h ph
2 stoweidlem39.2 
 |-  F/ t ph
3 stoweidlem39.3 
 |-  F/ w ph
4 stoweidlem39.4 
 |-  U = ( T \ B )
5 stoweidlem39.5 
 |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
6 stoweidlem39.6 
 |-  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 ) ) }
7 stoweidlem39.7 
 |-  ( ph -> r e. ( ~P W i^i Fin ) )
8 stoweidlem39.8 
 |-  ( ph -> D C_ U. r )
9 stoweidlem39.9 
 |-  ( ph -> D =/= (/) )
10 stoweidlem39.10 
 |-  ( ph -> E e. RR+ )
11 stoweidlem39.11 
 |-  ( ph -> B C_ T )
12 stoweidlem39.12 
 |-  ( ph -> W e. _V )
13 stoweidlem39.13 
 |-  ( ph -> A e. _V )
14 8 9 jca 
 |-  ( ph -> ( D C_ U. r /\ D =/= (/) ) )
15 ssn0 
 |-  ( ( D C_ U. r /\ D =/= (/) ) -> U. r =/= (/) )
16 unieq 
 |-  ( r = (/) -> U. r = U. (/) )
17 uni0 
 |-  U. (/) = (/)
18 16 17 eqtrdi 
 |-  ( r = (/) -> U. r = (/) )
19 18 necon3i 
 |-  ( U. r =/= (/) -> r =/= (/) )
20 14 15 19 3syl 
 |-  ( ph -> r =/= (/) )
21 20 neneqd 
 |-  ( ph -> -. r = (/) )
22 elinel2 
 |-  ( r e. ( ~P W i^i Fin ) -> r e. Fin )
23 7 22 syl 
 |-  ( ph -> r e. Fin )
24 fz1f1o 
 |-  ( r e. Fin -> ( r = (/) \/ ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) ) )
25 pm2.53 
 |-  ( ( r = (/) \/ ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) ) -> ( -. r = (/) -> ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) ) )
26 23 24 25 3syl 
 |-  ( ph -> ( -. r = (/) -> ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) ) )
27 21 26 mpd 
 |-  ( ph -> ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) )
28 oveq2 
 |-  ( m = ( # ` r ) -> ( 1 ... m ) = ( 1 ... ( # ` r ) ) )
29 28 f1oeq2d 
 |-  ( m = ( # ` r ) -> ( v : ( 1 ... m ) -1-1-onto-> r <-> v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) )
30 29 exbidv 
 |-  ( m = ( # ` r ) -> ( E. v v : ( 1 ... m ) -1-1-onto-> r <-> E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) )
31 30 rspcev 
 |-  ( ( ( # ` r ) e. NN /\ E. v v : ( 1 ... ( # ` r ) ) -1-1-onto-> r ) -> E. m e. NN E. v v : ( 1 ... m ) -1-1-onto-> r )
32 27 31 syl 
 |-  ( ph -> E. m e. NN E. v v : ( 1 ... m ) -1-1-onto-> r )
33 f1of 
 |-  ( v : ( 1 ... m ) -1-1-onto-> r -> v : ( 1 ... m ) --> r )
34 33 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> v : ( 1 ... m ) --> r )
35 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> ph )
36 elinel1 
 |-  ( r e. ( ~P W i^i Fin ) -> r e. ~P W )
37 36 elpwid 
 |-  ( r e. ( ~P W i^i Fin ) -> r C_ W )
38 35 7 37 3syl 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> r C_ W )
39 34 38 fssd 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> v : ( 1 ... m ) --> W )
40 8 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> D C_ U. r )
41 dff1o2 
 |-  ( v : ( 1 ... m ) -1-1-onto-> r <-> ( v Fn ( 1 ... m ) /\ Fun `' v /\ ran v = r ) )
42 41 simp3bi 
 |-  ( v : ( 1 ... m ) -1-1-onto-> r -> ran v = r )
43 42 unieqd 
 |-  ( v : ( 1 ... m ) -1-1-onto-> r -> U. ran v = U. r )
44 43 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> U. ran v = U. r )
45 40 44 sseqtrrd 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> D C_ U. ran v )
46 nfv 
 |-  F/ h m e. NN
47 1 46 nfan 
 |-  F/ h ( ph /\ m e. NN )
48 nfv 
 |-  F/ h v : ( 1 ... m ) -1-1-onto-> r
49 47 48 nfan 
 |-  F/ h ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r )
50 nfv 
 |-  F/ t m e. NN
51 2 50 nfan 
 |-  F/ t ( ph /\ m e. NN )
52 nfv 
 |-  F/ t v : ( 1 ... m ) -1-1-onto-> r
53 51 52 nfan 
 |-  F/ t ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r )
54 nfv 
 |-  F/ w m e. NN
55 3 54 nfan 
 |-  F/ w ( ph /\ m e. NN )
56 nfv 
 |-  F/ w v : ( 1 ... m ) -1-1-onto-> r
57 55 56 nfan 
 |-  F/ w ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r )
58 eqid 
 |-  ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } ) = ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } )
59 simplr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> m e. NN )
60 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> v : ( 1 ... m ) -1-1-onto-> r )
61 10 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> E e. RR+ )
62 11 sselda 
 |-  ( ( ph /\ b e. B ) -> b e. T )
63 notnot 
 |-  ( b e. B -> -. -. b e. B )
64 63 intnand 
 |-  ( b e. B -> -. ( b e. T /\ -. b e. B ) )
65 64 adantl 
 |-  ( ( ph /\ b e. B ) -> -. ( b e. T /\ -. b e. B ) )
66 eldif 
 |-  ( b e. ( T \ B ) <-> ( b e. T /\ -. b e. B ) )
67 65 66 sylnibr 
 |-  ( ( ph /\ b e. B ) -> -. b e. ( T \ B ) )
68 4 eleq2i 
 |-  ( b e. U <-> b e. ( T \ B ) )
69 67 68 sylnibr 
 |-  ( ( ph /\ b e. B ) -> -. b e. U )
70 62 69 eldifd 
 |-  ( ( ph /\ b e. B ) -> b e. ( T \ U ) )
71 70 ralrimiva 
 |-  ( ph -> A. b e. B b e. ( T \ U ) )
72 dfss3 
 |-  ( B C_ ( T \ U ) <-> A. b e. B b e. ( T \ U ) )
73 71 72 sylibr 
 |-  ( ph -> B C_ ( T \ U ) )
74 73 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> B C_ ( T \ U ) )
75 12 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> W e. _V )
76 13 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> A e. _V )
77 23 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> r e. Fin )
78 mptfi 
 |-  ( r e. Fin -> ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } ) e. Fin )
79 rnfi 
 |-  ( ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } ) e. Fin -> ran ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } ) e. Fin )
80 77 78 79 3syl 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> ran ( w e. r |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / m ) /\ A. t e. ( T \ U ) ( 1 - ( E / m ) ) < ( h ` t ) ) } ) e. Fin )
81 49 53 57 5 6 58 38 59 60 61 74 75 76 80 stoweidlem31 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) )
82 39 45 81 3jca 
 |-  ( ( ( ph /\ m e. NN ) /\ v : ( 1 ... m ) -1-1-onto-> r ) -> ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) )
83 82 ex 
 |-  ( ( ph /\ m e. NN ) -> ( v : ( 1 ... m ) -1-1-onto-> r -> ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) ) )
84 83 eximdv 
 |-  ( ( ph /\ m e. NN ) -> ( E. v v : ( 1 ... m ) -1-1-onto-> r -> E. v ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) ) )
85 84 reximdva 
 |-  ( ph -> ( E. m e. NN E. v v : ( 1 ... m ) -1-1-onto-> r -> E. m e. NN E. v ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) ) )
86 32 85 mpd 
 |-  ( ph -> E. m e. NN E. v ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ E. x ( x : ( 1 ... m ) --> Y /\ A. i e. ( 1 ... m ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( x ` i ) ` t ) ) ) ) )