Theorem stowei

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. The deduction version of this theorem is stoweid : often times it will be better to use stoweid in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stowei.1	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stowei.2	⊢ 𝐽 ∈ Comp
	stowei.3	⊢ 𝑇 = ∪ 𝐽
	stowei.4	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stowei.5	⊢ 𝐴 ⊆ 𝐶
	stowei.6	⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stowei.7	⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stowei.8	⊢ ( 𝑥 ∈ ℝ → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
	stowei.9	⊢ ( ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) → ∃ ℎ ∈ 𝐴 ( ℎ ‘ 𝑟 ) ≠ ( ℎ ‘ 𝑡 ) )
	stowei.10	⊢ 𝐹 ∈ 𝐶
	stowei.11	⊢ 𝐸 ∈ ℝ+
Assertion	stowei	⊢ ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸

Proof

Step	Hyp	Ref	Expression
1		stowei.1	⊢ 𝐾 = ( topGen ‘ ran (,) )
2		stowei.2	⊢ 𝐽 ∈ Comp
3		stowei.3	⊢ 𝑇 = ∪ 𝐽
4		stowei.4	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
5		stowei.5	⊢ 𝐴 ⊆ 𝐶
6		stowei.6	⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
7		stowei.7	⊢ ( ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
8		stowei.8	⊢ ( 𝑥 ∈ ℝ → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
9		stowei.9	⊢ ( ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) → ∃ ℎ ∈ 𝐴 ( ℎ ‘ 𝑟 ) ≠ ( ℎ ‘ 𝑡 ) )
10		stowei.10	⊢ 𝐹 ∈ 𝐶
11		stowei.11	⊢ 𝐸 ∈ ℝ+
12		nfcv	⊢ Ⅎ 𝑡 𝐹
13		nftru	⊢ Ⅎ 𝑡 ⊤
14	2	a1i	⊢ ( ⊤ → 𝐽 ∈ Comp )
15	5	a1i	⊢ ( ⊤ → 𝐴 ⊆ 𝐶 )
16	6	3adant1	⊢ ( ( ⊤ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
17	7	3adant1	⊢ ( ( ⊤ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
18	8	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
19	9	adantl	⊢ ( ( ⊤ ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ ℎ ∈ 𝐴 ( ℎ ‘ 𝑟 ) ≠ ( ℎ ‘ 𝑡 ) )
20	10	a1i	⊢ ( ⊤ → 𝐹 ∈ 𝐶 )
21	11	a1i	⊢ ( ⊤ → 𝐸 ∈ ℝ+ )
22	12 13 1 14 3 4 15 16 17 18 19 20 21	stoweid	⊢ ( ⊤ → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
23	22	mptru	⊢ ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸