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	eqtrid	⊢ ( 𝜑 → 𝐺 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐻 ‘ 𝑡 ) + ( ( 𝑇 × { 𝑆 } ) ‘ 𝑡 ) ) ) )
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 ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )