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	$⊢ \underline{Ⅎ} t G$
	stoweidlem21.2	$⊢ \underline{Ⅎ} t H$
	stoweidlem21.3	$⊢ \underline{Ⅎ} t S$
	stoweidlem21.4	$⊢ Ⅎ t φ$
	stoweidlem21.5	$⊢ G = (t \in T ⟼ H (t) + S)$
	stoweidlem21.6	$⊢ φ \to F : T ⟶ ℝ$
	stoweidlem21.7	$⊢ φ \to S \in ℝ$
	stoweidlem21.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweidlem21.9	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweidlem21.10	$⊢ φ \to \forall f \in A f : T ⟶ ℝ$
	stoweidlem21.11	$⊢ φ \to H \in A$
	stoweidlem21.12	$⊢ φ \to \forall t \in T \|H (t) - (F (t) - S)\| < E$
Assertion	stoweidlem21	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem21.1	$⊢ \underline{Ⅎ} t G$
2		stoweidlem21.2	$⊢ \underline{Ⅎ} t H$
3		stoweidlem21.3	$⊢ \underline{Ⅎ} t S$
4		stoweidlem21.4	$⊢ Ⅎ t φ$
5		stoweidlem21.5	$⊢ G = (t \in T ⟼ H (t) + S)$
6		stoweidlem21.6	$⊢ φ \to F : T ⟶ ℝ$
7		stoweidlem21.7	$⊢ φ \to S \in ℝ$
8		stoweidlem21.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweidlem21.9	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
10		stoweidlem21.10	$⊢ φ \to \forall f \in A f : T ⟶ ℝ$
11		stoweidlem21.11	$⊢ φ \to H \in A$
12		stoweidlem21.12	$⊢ φ \to \forall t \in T \|H (t) - (F (t) - S)\| < E$
13		fvconst2g	$⊢ (S \in ℝ \land t \in T) \to (T \times \{S\}) (t) = S$
14	7 13	sylan	$⊢ (φ \land t \in T) \to (T \times \{S\}) (t) = S$
15	14	eqcomd	$⊢ (φ \land t \in T) \to S = (T \times \{S\}) (t)$
16	15	oveq2d	$⊢ (φ \land t \in T) \to H (t) + S = H (t) + (T \times \{S\}) (t)$
17	4 16	mpteq2da	$⊢ φ \to (t \in T ⟼ H (t) + S) = (t \in T ⟼ H (t) + (T \times \{S\}) (t))$
18	5 17	syl5eq	$⊢ φ \to G = (t \in T ⟼ H (t) + (T \times \{S\}) (t))$
19		fconstmpt	$⊢ T \times \{S\} = (s \in T ⟼ S)$
20		nfcv	$⊢ \underline{Ⅎ} s S$
21		eqidd	$⊢ s = t \to S = S$
22	3 20 21	cbvmpt	$⊢ (s \in T ⟼ S) = (t \in T ⟼ S)$
23	19 22	eqtri	$⊢ T \times \{S\} = (t \in T ⟼ S)$
24	3	nfeq2	$⊢ Ⅎ t x = S$
25		simpl	$⊢ (x = S \land t \in T) \to x = S$
26	24 25	mpteq2da	$⊢ x = S \to (t \in T ⟼ x) = (t \in T ⟼ S)$
27	26	eleq1d	$⊢ x = S \to ((t \in T ⟼ x) \in A \leftrightarrow (t \in T ⟼ S) \in A)$
28	27	imbi2d	$⊢ x = S \to ((φ \to (t \in T ⟼ x) \in A) \leftrightarrow (φ \to (t \in T ⟼ S) \in A))$
29	9	expcom	$⊢ x \in ℝ \to (φ \to (t \in T ⟼ x) \in A)$
30	28 29	vtoclga	$⊢ S \in ℝ \to (φ \to (t \in T ⟼ S) \in A)$
31	7 30	mpcom	$⊢ φ \to (t \in T ⟼ S) \in A$
32	23 31	eqeltrid	$⊢ φ \to T \times \{S\} \in A$
33		nfcv	$⊢ \underline{Ⅎ} t T$
34	3	nfsn	$⊢ \underline{Ⅎ} t \{S\}$
35	33 34	nfxp	$⊢ \underline{Ⅎ} t (T \times \{S\})$
36	8 2 35	stoweidlem8	$⊢ (φ \land H \in A \land T \times \{S\} \in A) \to (t \in T ⟼ H (t) + (T \times \{S\}) (t)) \in A$
37	11 32 36	mpd3an23	$⊢ φ \to (t \in T ⟼ H (t) + (T \times \{S\}) (t)) \in A$
38	18 37	eqeltrd	$⊢ φ \to G \in A$
39		simpr	$⊢ (φ \land t \in T) \to t \in T$
40		feq1	$⊢ f = H \to (f : T ⟶ ℝ \leftrightarrow H : T ⟶ ℝ)$
41	40	rspccva	$⊢ (\forall f \in A f : T ⟶ ℝ \land H \in A) \to H : T ⟶ ℝ$
42	10 11 41	syl2anc	$⊢ φ \to H : T ⟶ ℝ$
43	42	ffvelrnda	$⊢ (φ \land t \in T) \to H (t) \in ℝ$
44	7	adantr	$⊢ (φ \land t \in T) \to S \in ℝ$
45	43 44	readdcld	$⊢ (φ \land t \in T) \to H (t) + S \in ℝ$
46	5	fvmpt2	$⊢ (t \in T \land H (t) + S \in ℝ) \to G (t) = H (t) + S$
47	39 45 46	syl2anc	$⊢ (φ \land t \in T) \to G (t) = H (t) + S$
48	47	oveq1d	$⊢ (φ \land t \in T) \to G (t) - F (t) = H (t) + S - F (t)$
49	43	recnd	$⊢ (φ \land t \in T) \to H (t) \in ℂ$
50	6	ffvelrnda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
51	50	recnd	$⊢ (φ \land t \in T) \to F (t) \in ℂ$
52	7	recnd	$⊢ φ \to S \in ℂ$
53	52	adantr	$⊢ (φ \land t \in T) \to S \in ℂ$
54	49 51 53	subsub3d	$⊢ (φ \land t \in T) \to H (t) - (F (t) - S) = H (t) + S - F (t)$
55	48 54	eqtr4d	$⊢ (φ \land t \in T) \to G (t) - F (t) = H (t) - (F (t) - S)$
56	55	fveq2d	$⊢ (φ \land t \in T) \to \|G (t) - F (t)\| = \|H (t) - (F (t) - S)\|$
57	12	r19.21bi	$⊢ (φ \land t \in T) \to \|H (t) - (F (t) - S)\| < E$
58	56 57	eqbrtrd	$⊢ (φ \land t \in T) \to \|G (t) - F (t)\| < E$
59	58	ex	$⊢ φ \to (t \in T \to \|G (t) - F (t)\| < E)$
60	4 59	ralrimi	$⊢ φ \to \forall t \in T \|G (t) - F (t)\| < E$
61	1	nfeq2	$⊢ Ⅎ t f = G$
62		fveq1	$⊢ f = G \to f (t) = G (t)$
63	62	oveq1d	$⊢ f = G \to f (t) - F (t) = G (t) - F (t)$
64	63	fveq2d	$⊢ f = G \to \|f (t) - F (t)\| = \|G (t) - F (t)\|$
65	64	breq1d	$⊢ f = G \to (\|f (t) - F (t)\| < E \leftrightarrow \|G (t) - F (t)\| < E)$
66	61 65	ralbid	$⊢ f = G \to (\forall t \in T \|f (t) - F (t)\| < E \leftrightarrow \forall t \in T \|G (t) - F (t)\| < E)$
67	66	rspcev	$⊢ (G \in A \land \forall t \in T \|G (t) - F (t)\| < E) \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$
68	38 60 67	syl2anc	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$

Metamath Proof Explorer

Theorem stoweidlem21

Proof