stoweid

Description: This theorem proves the Stone-Weierstrass theorem for real-valued functions: let J be a compact topology on T , and C be the set of real continuous functions on T . Assume that A is a subalgebra of C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if r and t are distinct points in T , then there exists a function h in A such that h(r) is distinct from h(t) ). Then, for any continuous function F and for any positive real E , there exists a function f in the subalgebra A , such that f approximates F up to E ( E represents the usual ε value). As a classical example, given any a, b reals, the closed interval T = [ a , b ] could be taken, along with the subalgebra A of real polynomials on T , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [ a , b ] . The proof and lemmas are written following BrosowskiDeutsh p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweid.1	$⊢ \underline{Ⅎ} t F$
	stoweid.2	$⊢ Ⅎ t φ$
	stoweid.3	$⊢ K = topGen (ran (.))$
	stoweid.4	$⊢ φ \to J \in Comp$
	stoweid.5	$⊢ T = ⋃ J$
	stoweid.6	$⊢ C = J Cn K$
	stoweid.7	$⊢ φ \to A \subseteq C$
	stoweid.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
	stoweid.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
	stoweid.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	stoweid.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists h \in A h (r) \neq h (t)$
	stoweid.12	$⊢ φ \to F \in C$
	stoweid.13	$⊢ φ \to E \in ℝ^{+}$
Assertion	stoweid	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$

Proof

Step	Hyp	Ref	Expression
1		stoweid.1	$⊢ \underline{Ⅎ} t F$
2		stoweid.2	$⊢ Ⅎ t φ$
3		stoweid.3	$⊢ K = topGen (ran (.))$
4		stoweid.4	$⊢ φ \to J \in Comp$
5		stoweid.5	$⊢ T = ⋃ J$
6		stoweid.6	$⊢ C = J Cn K$
7		stoweid.7	$⊢ φ \to A \subseteq C$
8		stoweid.8	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
9		stoweid.9	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
10		stoweid.10	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
11		stoweid.11	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists h \in A h (r) \neq h (t)$
12		stoweid.12	$⊢ φ \to F \in C$
13		stoweid.13	$⊢ φ \to E \in ℝ^{+}$
14		simpr	$⊢ (φ \land T = \emptyset) \to T = \emptyset$
15	10	ralrimiva	$⊢ φ \to \forall x \in ℝ (t \in T ⟼ x) \in A$
16		1re	$⊢ 1 \in ℝ$
17		id	$⊢ x = 1 \to x = 1$
18	17	mpteq2dv	$⊢ x = 1 \to (t \in T ⟼ x) = (t \in T ⟼ 1)$
19	18	eleq1d	$⊢ x = 1 \to ((t \in T ⟼ x) \in A \leftrightarrow (t \in T ⟼ 1) \in A)$
20	19	rspccv	$⊢ \forall x \in ℝ (t \in T ⟼ x) \in A \to (1 \in ℝ \to (t \in T ⟼ 1) \in A)$
21	15 16 20	mpisyl	$⊢ φ \to (t \in T ⟼ 1) \in A$
22	21	adantr	$⊢ (φ \land T = \emptyset) \to (t \in T ⟼ 1) \in A$
23	14 22	stoweidlem9	$⊢ (φ \land T = \emptyset) \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4})$
24		nfv	$⊢ Ⅎ f φ$
25		nfv	$⊢ Ⅎ f \neg T = \emptyset$
26	24 25	nfan	$⊢ Ⅎ f (φ \land \neg T = \emptyset)$
27		nfv	$⊢ Ⅎ t \neg T = \emptyset$
28	2 27	nfan	$⊢ Ⅎ t (φ \land \neg T = \emptyset)$
29		eqid	$⊢ (t \in T ⟼ F (t) - sup (ran F ℝ <)) = (t \in T ⟼ F (t) - sup (ran F ℝ <))$
30	4	adantr	$⊢ (φ \land \neg T = \emptyset) \to J \in Comp$
31	7	adantr	$⊢ (φ \land \neg T = \emptyset) \to A \subseteq C$
32	8	3adant1r	$⊢ ((φ \land \neg T = \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
33	9	3adant1r	$⊢ ((φ \land \neg T = \emptyset) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
34	10	adantlr	$⊢ ((φ \land \neg T = \emptyset) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
35	11	adantlr	$⊢ ((φ \land \neg T = \emptyset) \land (r \in T \land t \in T \land r \neq t)) \to \exists h \in A h (r) \neq h (t)$
36	12	adantr	$⊢ (φ \land \neg T = \emptyset) \to F \in C$
37		4re	$⊢ 4 \in ℝ$
38		4pos	$⊢ 0 < 4$
39	37 38	elrpii	$⊢ 4 \in ℝ^{+}$
40	39	a1i	$⊢ φ \to 4 \in ℝ^{+}$
41	40	rpreccld	$⊢ φ \to \frac{1}{4} \in ℝ^{+}$
42	13 41	ifcld	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ^{+}$
43	42	adantr	$⊢ (φ \land \neg T = \emptyset) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ^{+}$
44		neqne	$⊢ \neg T = \emptyset \to T \neq \emptyset$
45	44	adantl	$⊢ (φ \land \neg T = \emptyset) \to T \neq \emptyset$
46	13	rpred	$⊢ φ \to E \in ℝ$
47		4ne0	$⊢ 4 \neq 0$
48	37 47	rereccli	$⊢ \frac{1}{4} \in ℝ$
49	48	a1i	$⊢ φ \to \frac{1}{4} \in ℝ$
50	46 49	ifcld	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ$
51		3re	$⊢ 3 \in ℝ$
52		3ne0	$⊢ 3 \neq 0$
53	51 52	rereccli	$⊢ \frac{1}{3} \in ℝ$
54	53	a1i	$⊢ φ \to \frac{1}{3} \in ℝ$
55	13	rpxrd	$⊢ φ \to E \in ℝ^{*}$
56	41	rpxrd	$⊢ φ \to \frac{1}{4} \in ℝ^{*}$
57		xrmin2	$⊢ (E \in ℝ^{} \land \frac{1}{4} \in ℝ^{}) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq \frac{1}{4}$
58	55 56 57	syl2anc	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq \frac{1}{4}$
59		3lt4	$⊢ 3 < 4$
60		3pos	$⊢ 0 < 3$
61	51 37 60 38	ltrecii	$⊢ 3 < 4 \leftrightarrow \frac{1}{4} < \frac{1}{3}$
62	59 61	mpbi	$⊢ \frac{1}{4} < \frac{1}{3}$
63	62	a1i	$⊢ φ \to \frac{1}{4} < \frac{1}{3}$
64	50 49 54 58 63	lelttrd	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) < \frac{1}{3}$
65	64	adantr	$⊢ (φ \land \neg T = \emptyset) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) < \frac{1}{3}$
66	1 26 28 29 3 5 30 6 31 32 33 34 35 36 43 45 65	stoweidlem62	$⊢ (φ \land \neg T = \emptyset) \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4})$
67	23 66	pm2.61dan	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4})$
68		nfv	$⊢ Ⅎ t f \in A$
69	2 68	nfan	$⊢ Ⅎ t (φ \land f \in A)$
70		xrmin1	$⊢ (E \in ℝ^{} \land \frac{1}{4} \in ℝ^{}) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq E$
71	55 56 70	syl2anc	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq E$
72	71	ad2antrr	$⊢ ((φ \land f \in A) \land t \in T) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq E$
73	7	ad2antrr	$⊢ ((φ \land f \in A) \land t \in T) \to A \subseteq C$
74		simplr	$⊢ ((φ \land f \in A) \land t \in T) \to f \in A$
75	73 74	sseldd	$⊢ ((φ \land f \in A) \land t \in T) \to f \in C$
76	3 5 6 75	fcnre	$⊢ ((φ \land f \in A) \land t \in T) \to f : T ⟶ ℝ$
77		simpr	$⊢ ((φ \land f \in A) \land t \in T) \to t \in T$
78	76 77	jca	$⊢ ((φ \land f \in A) \land t \in T) \to (f : T ⟶ ℝ \land t \in T)$
79		ffvelrn	$⊢ (f : T ⟶ ℝ \land t \in T) \to f (t) \in ℝ$
80		recn	$⊢ f (t) \in ℝ \to f (t) \in ℂ$
81	78 79 80	3syl	$⊢ ((φ \land f \in A) \land t \in T) \to f (t) \in ℂ$
82	12	ad2antrr	$⊢ ((φ \land f \in A) \land t \in T) \to F \in C$
83	3 5 6 82	fcnre	$⊢ ((φ \land f \in A) \land t \in T) \to F : T ⟶ ℝ$
84	83 77	jca	$⊢ ((φ \land f \in A) \land t \in T) \to (F : T ⟶ ℝ \land t \in T)$
85		ffvelrn	$⊢ (F : T ⟶ ℝ \land t \in T) \to F (t) \in ℝ$
86		recn	$⊢ F (t) \in ℝ \to F (t) \in ℂ$
87	84 85 86	3syl	$⊢ ((φ \land f \in A) \land t \in T) \to F (t) \in ℂ$
88	81 87	subcld	$⊢ ((φ \land f \in A) \land t \in T) \to f (t) - F (t) \in ℂ$
89	88	abscld	$⊢ ((φ \land f \in A) \land t \in T) \to \|f (t) - F (t)\| \in ℝ$
90	16 37 47	3pm3.2i	$⊢ (1 \in ℝ \land 4 \in ℝ \land 4 \neq 0)$
91		redivcl	$⊢ (1 \in ℝ \land 4 \in ℝ \land 4 \neq 0) \to \frac{1}{4} \in ℝ$
92	90 91	mp1i	$⊢ φ \to \frac{1}{4} \in ℝ$
93	46 92	ifcld	$⊢ φ \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ$
94	93	ad2antrr	$⊢ ((φ \land f \in A) \land t \in T) \to if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ$
95	46	ad2antrr	$⊢ ((φ \land f \in A) \land t \in T) \to E \in ℝ$
96		ltletr	$⊢ (\|f (t) - F (t)\| \in ℝ \land if (E \leq \frac{1}{4}, E, \frac{1}{4}) \in ℝ \land E \in ℝ) \to ((\|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4}) \land if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq E) \to \|f (t) - F (t)\| < E)$
97	89 94 95 96	syl3anc	$⊢ ((φ \land f \in A) \land t \in T) \to ((\|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4}) \land if (E \leq \frac{1}{4}, E, \frac{1}{4}) \leq E) \to \|f (t) - F (t)\| < E)$
98	72 97	mpan2d	$⊢ ((φ \land f \in A) \land t \in T) \to (\|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4}) \to \|f (t) - F (t)\| < E)$
99	69 98	ralimdaa	$⊢ (φ \land f \in A) \to (\forall t \in T \|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4}) \to \forall t \in T \|f (t) - F (t)\| < E)$
100	99	reximdva	$⊢ φ \to (\exists f \in A \forall t \in T \|f (t) - F (t)\| < if (E \leq \frac{1}{4}, E, \frac{1}{4}) \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E)$
101	67 100	mpd	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$

Metamath Proof Explorer

Theorem stoweid

Proof