Theorem stoweidlem21 46834

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
stoweidlem21	⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)

Distinct variable groups:   𝑓,𝑔,𝑡,𝑇   𝐴,𝑓,𝑔   𝑓,𝐸,𝑔   𝑓,𝐹,𝑔   𝑓,𝐺,𝑔   𝑓,𝐻,𝑔   𝜑,𝑓,𝑔   𝑆,𝑔   𝑥,𝑡,𝑇   𝑥,𝐴   𝑥,𝑆   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑡)   𝐴(𝑡)   𝑆(𝑡, 𝑓)   𝐸(𝑥, 𝑡)   𝐹(𝑥, 𝑡)   𝐺(𝑥, 𝑡)   𝐻(𝑥, 𝑡)

Proof of Theorem stoweidlem21

Dummy variable 𝑠 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem21.5	. . . 4 ⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + 𝑆))
2		stoweidlem21.4	. . . . 5 ⊢ Ⅎ𝑡𝜑
3		stoweidlem21.7	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ ℝ)
4		fvconst2g 7204	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ ∧ 𝑡 ∈ 𝑇) → ((𝑇 × {𝑆})‘𝑡) = 𝑆)
5	3, 4	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑇 × {𝑆})‘𝑡) = 𝑆)
6	5	eqcomd 2768	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 = ((𝑇 × {𝑆})‘𝑡))
7	6	oveq2d 7432	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) + 𝑆) = ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡)))
8	2, 7	mpteq2da 5201	. . . 4 ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + 𝑆)) = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))))
9	1, 8	eqtrid 2809	. . 3 ⊢ (𝜑 → 𝐺 = (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))))
10		stoweidlem21.11	. . . 4 ⊢ (𝜑 → 𝐻 ∈ 𝐴)
11		fconstmpt 5721	. . . . . 6 ⊢ (𝑇 × {𝑆}) = (𝑠 ∈ 𝑇 ↦ 𝑆)
12		stoweidlem21.3	. . . . . . 7 ⊢ Ⅎ𝑡𝑆
13		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑠𝑆
14		eqidd 2763	. . . . . . 7 ⊢ (𝑠 = 𝑡 → 𝑆 = 𝑆)
15	12, 13, 14	cbvmpt 5211	. . . . . 6 ⊢ (𝑠 ∈ 𝑇 ↦ 𝑆) = (𝑡 ∈ 𝑇 ↦ 𝑆)
16	11, 15	eqtri 2785	. . . . 5 ⊢ (𝑇 × {𝑆}) = (𝑡 ∈ 𝑇 ↦ 𝑆)
17	12	nfeq2 2941	. . . . . . . . . 10 ⊢ Ⅎ𝑡 𝑥 = 𝑆
18		simpl 488	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑆 ∧ 𝑡 ∈ 𝑇) → 𝑥 = 𝑆)
19	17, 18	mpteq2da 5201	. . . . . . . . 9 ⊢ (𝑥 = 𝑆 → (𝑡 ∈ 𝑇 ↦ 𝑥) = (𝑡 ∈ 𝑇 ↦ 𝑆))
20	19	eleq1d 2847	. . . . . . . 8 ⊢ (𝑥 = 𝑆 → ((𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴))
21	20	imbi2d 343	. . . . . . 7 ⊢ (𝑥 = 𝑆 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)))
22		stoweidlem21.9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)
23	22	expcom 419	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴))
24	21, 23	vtoclga 3539	. . . . . 6 ⊢ (𝑆 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴))
25	3, 24	mpcom 39	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)
26	16, 25	eqeltrid 2866	. . . 4 ⊢ (𝜑 → (𝑇 × {𝑆}) ∈ 𝐴)
27		stoweidlem21.8	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
28		stoweidlem21.2	. . . . 5 ⊢ Ⅎ𝑡𝐻
29		nfcv 2924	. . . . . 6 ⊢ Ⅎ𝑡𝑇
30	12	nfsn 4671	. . . . . 6 ⊢ Ⅎ𝑡{𝑆}
31	29, 30	nfxp 5692	. . . . 5 ⊢ Ⅎ𝑡(𝑇 × {𝑆})
32	27, 28, 31	stoweidlem8 46821	. . . 4 ⊢ ((𝜑 ∧ 𝐻 ∈ 𝐴 ∧ (𝑇 × {𝑆}) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))) ∈ 𝐴)
33	10, 26, 32	mpd3an23 1492	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐻‘𝑡) + ((𝑇 × {𝑆})‘𝑡))) ∈ 𝐴)
34	9, 33	eqeltrd 2862	. 2 ⊢ (𝜑 → 𝐺 ∈ 𝐴)
35		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇)
36		stoweidlem21.10	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑓 ∈ 𝐴 𝑓:𝑇⟶ℝ)
37		feq1 6684	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐻 → (𝑓:𝑇⟶ℝ ↔ 𝐻:𝑇⟶ℝ))
38	37	rspccva 3578	. . . . . . . . . . . 12 ⊢ ((∀𝑓 ∈ 𝐴 𝑓:𝑇⟶ℝ ∧ 𝐻 ∈ 𝐴) → 𝐻:𝑇⟶ℝ)
39	36, 10, 38	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻:𝑇⟶ℝ)
40	39	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℝ)
41	3	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 ∈ ℝ)
42	40, 41	readdcld 11263	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) + 𝑆) ∈ ℝ)
43	1	fvmpt2 7002	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐻‘𝑡) + 𝑆) ∈ ℝ) → (𝐺‘𝑡) = ((𝐻‘𝑡) + 𝑆))
44	35, 42, 43	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑡) = ((𝐻‘𝑡) + 𝑆))
45	44	oveq1d 7431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑡) − (𝐹‘𝑡)) = (((𝐻‘𝑡) + 𝑆) − (𝐹‘𝑡)))
46	40	recnd 11262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) ∈ ℂ)
47		stoweidlem21.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
48	47	ffvelcdmda 7080	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ)
49	48	recnd 11262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ)
50	3	recnd 11262	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ ℂ)
51	50	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑆 ∈ ℂ)
52	46, 49, 51	subsub3d 11624	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆)) = (((𝐻‘𝑡) + 𝑆) − (𝐹‘𝑡)))
53	45, 52	eqtr4d 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑡) − (𝐹‘𝑡)) = ((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆)))
54	53	fveq2d 6886	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) = (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))))
55		stoweidlem21.12	. . . . . 6 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) < 𝐸)
56	55	r19.21bi 3256	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐻‘𝑡) − ((𝐹‘𝑡) − 𝑆))) < 𝐸)
57	54, 56	eqbrtrd 5131	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸)
58	57	ex 418	. . 3 ⊢ (𝜑 → (𝑡 ∈ 𝑇 → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸))
59	2, 58	ralrimi 3262	. 2 ⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸)
60		stoweidlem21.1	. . . . 5 ⊢ Ⅎ𝑡𝐺
61	60	nfeq2 2941	. . . 4 ⊢ Ⅎ𝑡 𝑓 = 𝐺
62		fveq1 6881	. . . . . . 7 ⊢ (𝑓 = 𝐺 → (𝑓‘𝑡) = (𝐺‘𝑡))
63	62	oveq1d 7431	. . . . . 6 ⊢ (𝑓 = 𝐺 → ((𝑓‘𝑡) − (𝐹‘𝑡)) = ((𝐺‘𝑡) − (𝐹‘𝑡)))
64	63	fveq2d 6886	. . . . 5 ⊢ (𝑓 = 𝐺 → (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) = (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))
65	64	breq1d 5117	. . . 4 ⊢ (𝑓 = 𝐺 → ((abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸 ↔ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸))
66	61, 65	ralbid 3277	. . 3 ⊢ (𝑓 = 𝐺 → (∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸 ↔ ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸))
67	66	rspcev 3579	. 2 ⊢ ((𝐺 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) < 𝐸) → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)
68	34, 59, 67	syl2anc 596	1 ⊢ (𝜑 → ∃𝑓 ∈ 𝐴 ∀𝑡 ∈ 𝑇 (abs‘((𝑓‘𝑡) − (𝐹‘𝑡))) < 𝐸)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2909  ∀wral 3078  ∃wrex 3088  {csn 4587   class class class wbr 5107   ↦ cmpt 5190   × cxp 5657  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  ℂcc 11123  ℝcr 11124   + caddc 11128   < clt 11268   − cmin 11466  abscabs 15321

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11270  df-mnf 11271  df-ltxr 11273  df-sub 11468

This theorem is used by:  stoweidlem62  46875