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 ⊢ Ⅎ 𝑡 𝐺
stoweidlem21.2 ⊢ Ⅎ 𝑡 𝐻
stoweidlem21.3 ⊢ Ⅎ 𝑡 𝑆
stoweidlem21.4 ⊢ Ⅎ 𝑡 𝜑
stoweidlem21.5 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) )
stoweidlem21.6 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
stoweidlem21.7 ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
stoweidlem21.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem21.9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem21.10 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐴 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem21.11 ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
stoweidlem21.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ) < 𝐸 )
Assertion stoweidlem21 ( 𝜑 → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )

Proof

Step Hyp Ref Expression
1 stoweidlem21.1 ⊢ Ⅎ 𝑡 𝐺
2 stoweidlem21.2 ⊢ Ⅎ 𝑡 𝐻
3 stoweidlem21.3 ⊢ Ⅎ 𝑡 𝑆
4 stoweidlem21.4 ⊢ Ⅎ 𝑡 𝜑
5 stoweidlem21.5 ⊢ 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) )
6 stoweidlem21.6 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
7 stoweidlem21.7 ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
8 stoweidlem21.8 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
9 stoweidlem21.9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
10 stoweidlem21.10 ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐴 𝑓 : 𝑇 ⟶ ℝ )
11 stoweidlem21.11 ⊢ ( 𝜑 → 𝐻 ∈ 𝐴 )
12 stoweidlem21.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ) < 𝐸 )
13 fvconst2g ⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) = 𝑆 )
14 7 13 sylan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) = 𝑆 )
15 14 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑆 = ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) )
16 15 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) = ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) )
17 4 16 mpteq2da ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) ) )
18 5 17 syl5eq ⊢ ( 𝜑 → 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) ) )
19 fconstmpt ⊢ ( 𝑇 × { 𝑆 } ) = ( 𝑠 ∈ 𝑇 ↦ 𝑆 )
20 nfcv ⊢ Ⅎ 𝑠 𝑆
21 eqidd ⊢ ( 𝑠 = 𝑡 → 𝑆 = 𝑆 )
22 3 20 21 cbvmpt ⊢ ( 𝑠 ∈ 𝑇 ↦ 𝑆 ) = ( 𝑡 ∈ 𝑇 ↦ 𝑆 )
23 19 22 eqtri ⊢ ( 𝑇 × { 𝑆 } ) = ( 𝑡 ∈ 𝑇 ↦ 𝑆 )
24 3 nfeq2 ⊢ Ⅎ 𝑡 𝑥 = 𝑆
25 simpl ⊢ ( ( 𝑥 = 𝑆 ∧ 𝑡 ∈ 𝑇 ) → 𝑥 = 𝑆 )
26 24 25 mpteq2da ⊢ ( 𝑥 = 𝑆 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) = ( 𝑡 ∈ 𝑇 ↦ 𝑆 ) )
27 26 eleq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ 𝑆 ) ∈ 𝐴 ) )
28 27 imbi2d ⊢ ( 𝑥 = 𝑆 → ( ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑆 ) ∈ 𝐴 ) ) )
29 9 expcom ⊢ ( 𝑥 ∈ ℝ → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) )
30 28 29 vtoclga ⊢ ( 𝑆 ∈ ℝ → ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑆 ) ∈ 𝐴 ) )
31 7 30 mpcom ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ 𝑆 ) ∈ 𝐴 )
32 23 31 eqeltrid ⊢ ( 𝜑 → ( 𝑇 × { 𝑆 } ) ∈ 𝐴 )
33 nfcv ⊢ Ⅎ 𝑡 𝑇
34 3 nfsn ⊢ Ⅎ 𝑡 { 𝑆 }
35 33 34 nfxp ⊢ Ⅎ 𝑡 ( 𝑇 × { 𝑆 } )
36 8 2 35 stoweidlem8 ⊢ ( ( 𝜑 ∧ 𝐻 ∈ 𝐴 ∧ ( 𝑇 × { 𝑆 } ) ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
37 11 32 36 mpd3an23 ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
38 18 37 eqeltrd ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
40 feq1 ⊢ ( 𝑓 = 𝐻 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝐻 : 𝑇 ⟶ ℝ ) )
41 40 rspccva ⊢ ( ( ∀ 𝑓 ∈ 𝐴 𝑓 : 𝑇 ⟶ ℝ ∧ 𝐻 ∈ 𝐴 ) → 𝐻 : 𝑇 ⟶ ℝ )
42 10 11 41 syl2anc ⊢ ( 𝜑 → 𝐻 : 𝑇 ⟶ ℝ )
43 42 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ∈ ℝ )
44 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑆 ∈ ℝ )
45 43 44 readdcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) ∈ ℝ )
46 5 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) )
47 39 45 46 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) = ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) )
48 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) = ( ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) − ( 𝐹 ‘ 𝑡 ) ) )
49 43 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) ∈ ℂ )
50 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
51 50 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
52 7 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑆 ∈ ℂ )
54 49 51 53 subsub3d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) = ( ( ( 𝐻 ‘ 𝑡 ) + 𝑆 ) − ( 𝐹 ‘ 𝑡 ) ) )
55 48 54 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) )
56 55 fveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ) )
57 12 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( 𝐻 ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − 𝑆 ) ) ) < 𝐸 )
58 56 57 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
59 58 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) )
60 4 59 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
61 1 nfeq2 ⊢ Ⅎ 𝑡 𝑓 = 𝐺
62 fveq1 ⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑡 ) )
63 62 oveq1d ⊢ ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) )
64 63 fveq2d ⊢ ( 𝑓 = 𝐺 → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) )
65 64 breq1d ⊢ ( 𝑓 = 𝐺 → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) )
66 61 65 ralbid ⊢ ( 𝑓 = 𝐺 → ( ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ↔ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) )
67 66 rspcev ⊢ ( ( 𝐺 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝐺 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 ) → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
68 38 60 67 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )