stoweidlem62

Description: This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows BrosowskiDeutsh p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017) (Revised by AV, 13-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		stoweidlem62.1	$⊢ \underline{Ⅎ} t F$
2		stoweidlem62.2	$⊢ Ⅎ f φ$
3		stoweidlem62.3	$⊢ Ⅎ t φ$
4		stoweidlem62.4	$⊢ H = (t \in T ⟼ F (t) - inf (ran F ℝ <))$
5		stoweidlem62.5	$⊢ K = topGen (ran (.))$
6		stoweidlem62.6	$⊢ T = ⋃ J$
7		stoweidlem62.7	$⊢ φ \to J \in Comp$
8		stoweidlem62.8	$⊢ C = J Cn K$
9		stoweidlem62.9	$⊢ φ \to A \subseteq C$
10		stoweidlem62.10	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
11		stoweidlem62.11	$⊢ (φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A$
12		stoweidlem62.12	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
13		stoweidlem62.13	$⊢ (φ \land (r \in T \land t \in T \land r \neq t)) \to \exists q \in A q (r) \neq q (t)$
14		stoweidlem62.14	$⊢ φ \to F \in C$
15		stoweidlem62.15	$⊢ φ \to E \in ℝ^{+}$
16		stoweidlem62.16	$⊢ φ \to T \neq \emptyset$
17		stoweidlem62.17	$⊢ φ \to E < \frac{1}{3}$
18		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ F (t) - inf (ran F ℝ <))$
19	4 18	nfcxfr	$⊢ \underline{Ⅎ} t H$
20		eleq1w	$⊢ g = h \to (g \in A \leftrightarrow h \in A)$
21	20	3anbi3d	$⊢ g = h \to ((φ \land f \in A \land g \in A) \leftrightarrow (φ \land f \in A \land h \in A))$
22		fveq1	$⊢ g = h \to g (t) = h (t)$
23	22	oveq2d	$⊢ g = h \to f (t) + g (t) = f (t) + h (t)$
24	23	mpteq2dv	$⊢ g = h \to (t \in T ⟼ f (t) + g (t)) = (t \in T ⟼ f (t) + h (t))$
25	24	eleq1d	$⊢ g = h \to ((t \in T ⟼ f (t) + g (t)) \in A \leftrightarrow (t \in T ⟼ f (t) + h (t)) \in A)$
26	21 25	imbi12d	$⊢ g = h \to (((φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A) \leftrightarrow ((φ \land f \in A \land h \in A) \to (t \in T ⟼ f (t) + h (t)) \in A))$
27	26 10	chvarvv	$⊢ (φ \land f \in A \land h \in A) \to (t \in T ⟼ f (t) + h (t)) \in A$
28	22	oveq2d	$⊢ g = h \to f (t) g (t) = f (t) h (t)$
29	28	mpteq2dv	$⊢ g = h \to (t \in T ⟼ f (t) g (t)) = (t \in T ⟼ f (t) h (t))$
30	29	eleq1d	$⊢ g = h \to ((t \in T ⟼ f (t) g (t)) \in A \leftrightarrow (t \in T ⟼ f (t) h (t)) \in A)$
31	21 30	imbi12d	$⊢ g = h \to (((φ \land f \in A \land g \in A) \to (t \in T ⟼ f (t) g (t)) \in A) \leftrightarrow ((φ \land f \in A \land h \in A) \to (t \in T ⟼ f (t) h (t)) \in A))$
32	31 11	chvarvv	$⊢ (φ \land f \in A \land h \in A) \to (t \in T ⟼ f (t) h (t)) \in A$
33	1	nfrn	$⊢ \underline{Ⅎ} t ran F$
34		nfcv	$⊢ \underline{Ⅎ} t ℝ$
35		nfcv	$⊢ \underline{Ⅎ} t <$
36	33 34 35	nfinf	$⊢ \underline{Ⅎ} t inf (ran F ℝ <)$
37		eqid	$⊢ T \times \{- inf (ran F ℝ <)\} = T \times \{- inf (ran F ℝ <)\}$
38		cmptop	$⊢ J \in Comp \to J \in Top$
39	7 38	syl	$⊢ φ \to J \in Top$
40	14 8	eleqtrdi	$⊢ φ \to F \in (J Cn K)$
41	1 3 6 5 7 40 16	stoweidlem29	$⊢ φ \to (inf (ran F ℝ <) \in ran F \land inf (ran F ℝ <) \in ℝ \land \forall t \in T inf (ran F ℝ <) \leq F (t))$
42	41	simp2d	$⊢ φ \to inf (ran F ℝ <) \in ℝ$
43	1 36 3 6 37 5 39 8 14 42	stoweidlem47	$⊢ φ \to (t \in T ⟼ F (t) - inf (ran F ℝ <)) \in C$
44	4 43	eqeltrid	$⊢ φ \to H \in C$
45	41	simp3d	$⊢ φ \to \forall t \in T inf (ran F ℝ <) \leq F (t)$
46	45	r19.21bi	$⊢ (φ \land t \in T) \to inf (ran F ℝ <) \leq F (t)$
47	5 6 8 14	fcnre	$⊢ φ \to F : T ⟶ ℝ$
48	47	ffvelcdmda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
49	42	adantr	$⊢ (φ \land t \in T) \to inf (ran F ℝ <) \in ℝ$
50	48 49	subge0d	$⊢ (φ \land t \in T) \to (0 \leq F (t) - inf (ran F ℝ <) \leftrightarrow inf (ran F ℝ <) \leq F (t))$
51	46 50	mpbird	$⊢ (φ \land t \in T) \to 0 \leq F (t) - inf (ran F ℝ <)$
52		simpr	$⊢ (φ \land t \in T) \to t \in T$
53	48 49	resubcld	$⊢ (φ \land t \in T) \to F (t) - inf (ran F ℝ <) \in ℝ$
54	4	fvmpt2	$⊢ (t \in T \land F (t) - inf (ran F ℝ <) \in ℝ) \to H (t) = F (t) - inf (ran F ℝ <)$
55	52 53 54	syl2anc	$⊢ (φ \land t \in T) \to H (t) = F (t) - inf (ran F ℝ <)$
56	51 55	breqtrrd	$⊢ (φ \land t \in T) \to 0 \leq H (t)$
57	56	ex	$⊢ φ \to (t \in T \to 0 \leq H (t))$
58	3 57	ralrimi	$⊢ φ \to \forall t \in T 0 \leq H (t)$
59	15	rphalfcld	$⊢ φ \to \frac{E}{2} \in ℝ^{+}$
60	15	rpred	$⊢ φ \to E \in ℝ$
61	60	rehalfcld	$⊢ φ \to \frac{E}{2} \in ℝ$
62		3re	$⊢ 3 \in ℝ$
63		3ne0	$⊢ 3 \neq 0$
64	62 63	rereccli	$⊢ \frac{1}{3} \in ℝ$
65	64	a1i	$⊢ φ \to \frac{1}{3} \in ℝ$
66		rphalflt	$⊢ E \in ℝ^{+} \to \frac{E}{2} < E$
67	15 66	syl	$⊢ φ \to \frac{E}{2} < E$
68	61 60 65 67 17	lttrd	$⊢ φ \to \frac{E}{2} < \frac{1}{3}$
69	19 3 5 7 6 16 8 9 27 32 12 13 44 58 59 68	stoweidlem61	$⊢ φ \to \exists h \in A \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2})$
70		nfra1	$⊢ Ⅎ t \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2})$
71	3 70	nfan	$⊢ Ⅎ t (φ \land \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2}))$
72		rsp	$⊢ \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2}) \to (t \in T \to \|h (t) - H (t)\| < 2 (\frac{E}{2}))$
73	15	rpcnd	$⊢ φ \to E \in ℂ$
74		2cnd	$⊢ φ \to 2 \in ℂ$
75		2ne0	$⊢ 2 \neq 0$
76	75	a1i	$⊢ φ \to 2 \neq 0$
77	73 74 76	divcan2d	$⊢ φ \to 2 (\frac{E}{2}) = E$
78	77	breq2d	$⊢ φ \to (\|h (t) - H (t)\| < 2 (\frac{E}{2}) \leftrightarrow \|h (t) - H (t)\| < E)$
79	78	biimpd	$⊢ φ \to (\|h (t) - H (t)\| < 2 (\frac{E}{2}) \to \|h (t) - H (t)\| < E)$
80	72 79	sylan9r	$⊢ (φ \land \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2})) \to (t \in T \to \|h (t) - H (t)\| < E)$
81	71 80	ralrimi	$⊢ (φ \land \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2})) \to \forall t \in T \|h (t) - H (t)\| < E$
82	81	ex	$⊢ φ \to (\forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2}) \to \forall t \in T \|h (t) - H (t)\| < E)$
83	82	reximdv	$⊢ φ \to (\exists h \in A \forall t \in T \|h (t) - H (t)\| < 2 (\frac{E}{2}) \to \exists h \in A \forall t \in T \|h (t) - H (t)\| < E)$
84	69 83	mpd	$⊢ φ \to \exists h \in A \forall t \in T \|h (t) - H (t)\| < E$
85		nfmpt1	$⊢ \underline{Ⅎ} t (t \in T ⟼ h (t) + inf (ran F ℝ <))$
86		nfcv	$⊢ \underline{Ⅎ} t h$
87		nfv	$⊢ Ⅎ t h \in A$
88		nfra1	$⊢ Ⅎ t \forall t \in T \|h (t) - H (t)\| < E$
89	87 88	nfan	$⊢ Ⅎ t (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)$
90	3 89	nfan	$⊢ Ⅎ t (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E))$
91		eqid	$⊢ (t \in T ⟼ h (t) + inf (ran F ℝ <)) = (t \in T ⟼ h (t) + inf (ran F ℝ <))$
92	47	adantr	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to F : T ⟶ ℝ$
93	42	adantr	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to inf (ran F ℝ <) \in ℝ$
94	10	3adant1r	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land f \in A \land g \in A) \to (t \in T ⟼ f (t) + g (t)) \in A$
95	12	adantlr	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land x \in ℝ) \to (t \in T ⟼ x) \in A$
96	9	sseld	$⊢ φ \to (f \in A \to f \in C)$
97	8	eleq2i	$⊢ f \in C \leftrightarrow f \in (J Cn K)$
98	96 97	imbitrdi	$⊢ φ \to (f \in A \to f \in (J Cn K))$
99		eqid	$⊢ ⋃ J = ⋃ J$
100		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
101	5	unieqi	$⊢ ⋃ K = ⋃ topGen (ran (.))$
102	100 101	eqtr4i	$⊢ ℝ = ⋃ K$
103	99 102	cnf	$⊢ f \in (J Cn K) \to f : ⋃ J ⟶ ℝ$
104	98 103	syl6	$⊢ φ \to (f \in A \to f : ⋃ J ⟶ ℝ)$
105		feq2	$⊢ T = ⋃ J \to (f : T ⟶ ℝ \leftrightarrow f : ⋃ J ⟶ ℝ)$
106	6 105	mp1i	$⊢ φ \to (f : T ⟶ ℝ \leftrightarrow f : ⋃ J ⟶ ℝ)$
107	104 106	sylibrd	$⊢ φ \to (f \in A \to f : T ⟶ ℝ)$
108	2 107	ralrimi	$⊢ φ \to \forall f \in A f : T ⟶ ℝ$
109	108	adantr	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to \forall f \in A f : T ⟶ ℝ$
110		simprl	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to h \in A$
111	55	eqcomd	$⊢ (φ \land t \in T) \to F (t) - inf (ran F ℝ <) = H (t)$
112	111	oveq2d	$⊢ (φ \land t \in T) \to h (t) - (F (t) - inf (ran F ℝ <)) = h (t) - H (t)$
113	112	fveq2d	$⊢ (φ \land t \in T) \to \|h (t) - (F (t) - inf (ran F ℝ <))\| = \|h (t) - H (t)\|$
114	113	adantlr	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land t \in T) \to \|h (t) - (F (t) - inf (ran F ℝ <))\| = \|h (t) - H (t)\|$
115		simplrr	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land t \in T) \to \forall t \in T \|h (t) - H (t)\| < E$
116		rspa	$⊢ (\forall t \in T \|h (t) - H (t)\| < E \land t \in T) \to \|h (t) - H (t)\| < E$
117	115 116	sylancom	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land t \in T) \to \|h (t) - H (t)\| < E$
118	114 117	eqbrtrd	$⊢ ((φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \land t \in T) \to \|h (t) - (F (t) - inf (ran F ℝ <))\| < E$
119	118	ex	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to (t \in T \to \|h (t) - (F (t) - inf (ran F ℝ <))\| < E)$
120	90 119	ralrimi	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to \forall t \in T \|h (t) - (F (t) - inf (ran F ℝ <))\| < E$
121	85 86 36 90 91 92 93 94 95 109 110 120	stoweidlem21	$⊢ (φ \land (h \in A \land \forall t \in T \|h (t) - H (t)\| < E)) \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$
122	84 121	rexlimddv	$⊢ φ \to \exists f \in A \forall t \in T \|f (t) - F (t)\| < E$

Metamath Proof Explorer

Theorem stoweidlem62

Proof