Theorem 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	⊢ Ⅎ 𝑡 𝐹
	stoweidlem62.2	⊢ Ⅎ 𝑓 𝜑
	stoweidlem62.3	⊢ Ⅎ 𝑡 𝜑
	stoweidlem62.4	⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
	stoweidlem62.5	⊢ 𝐾 = ( topGen ‘ ran (,) )
	stoweidlem62.6	⊢ 𝑇 = ∪ 𝐽
	stoweidlem62.7	⊢ ( 𝜑 → 𝐽 ∈ Comp )
	stoweidlem62.8	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
	stoweidlem62.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	stoweidlem62.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem62.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
	stoweidlem62.12	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
	stoweidlem62.13	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
	stoweidlem62.14	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
	stoweidlem62.15	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	stoweidlem62.16	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
	stoweidlem62.17	⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion	stoweidlem62	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem62.1	⊢ Ⅎ 𝑡 𝐹
2		stoweidlem62.2	⊢ Ⅎ 𝑓 𝜑
3		stoweidlem62.3	⊢ Ⅎ 𝑡 𝜑
4		stoweidlem62.4	⊢ 𝐻 = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
5		stoweidlem62.5	⊢ 𝐾 = ( topGen ‘ ran (,) )
6		stoweidlem62.6	⊢ 𝑇 = ∪ 𝐽
7		stoweidlem62.7	⊢ ( 𝜑 → 𝐽 ∈ Comp )
8		stoweidlem62.8	⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
9		stoweidlem62.9	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
10		stoweidlem62.10	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11		stoweidlem62.11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12		stoweidlem62.12	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
13		stoweidlem62.13	⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
14		stoweidlem62.14	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
15		stoweidlem62.15	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
16		stoweidlem62.16	⊢ ( 𝜑 → 𝑇 ≠ ∅ )
17		stoweidlem62.17	⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
18		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
19	4 18	nfcxfr	⊢ Ⅎ 𝑡 𝐻
20		eleq1w	⊢ ( 𝑔 = ℎ → ( 𝑔 ∈ 𝐴 ↔ ℎ ∈ 𝐴 ) )
21	20	3anbi3d	⊢ ( 𝑔 = ℎ → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ) )
22		fveq1	⊢ ( 𝑔 = ℎ → ( 𝑔 ‘ 𝑡 ) = ( ℎ ‘ 𝑡 ) )
23	22	oveq2d	⊢ ( 𝑔 = ℎ → ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝑓 ‘ 𝑡 ) + ( ℎ ‘ 𝑡 ) ) )
24	23	mpteq2dv	⊢ ( 𝑔 = ℎ → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( ℎ ‘ 𝑡 ) ) ) )
25	24	eleq1d	⊢ ( 𝑔 = ℎ → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
26	21 25	imbi12d	⊢ ( 𝑔 = ℎ → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
27	26 10	chvarvv	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 )
28	22	oveq2d	⊢ ( 𝑔 = ℎ → ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) = ( ( 𝑓 ‘ 𝑡 ) · ( ℎ ‘ 𝑡 ) ) )
29	28	mpteq2dv	⊢ ( 𝑔 = ℎ → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( ℎ ‘ 𝑡 ) ) ) )
30	29	eleq1d	⊢ ( 𝑔 = ℎ → ( ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 ) )
31	21 30	imbi12d	⊢ ( 𝑔 = ℎ → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 ) ) )
32	31 11	chvarvv	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( ℎ ‘ 𝑡 ) ) ) ∈ 𝐴 )
33	1	nfrn	⊢ Ⅎ 𝑡 ran 𝐹
34		nfcv	⊢ Ⅎ 𝑡 ℝ
35		nfcv	⊢ Ⅎ 𝑡 <
36	33 34 35	nfinf	⊢ Ⅎ 𝑡 inf ( ran 𝐹 , ℝ , < )
37		eqid	⊢ ( 𝑇 × { - inf ( ran 𝐹 , ℝ , < ) } ) = ( 𝑇 × { - inf ( ran 𝐹 , ℝ , < ) } )
38		cmptop	⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
39	7 38	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
40	14 8	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
41	1 3 6 5 7 40 16	stoweidlem29	⊢ ( 𝜑 → ( inf ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ∧ inf ( ran 𝐹 , ℝ , < ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
42	41	simp2d	⊢ ( 𝜑 → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
43	1 36 3 6 37 5 39 8 14 42	stoweidlem47	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ∈ 𝐶 )
44	4 43	eqeltrid	⊢ ( 𝜑 → 𝐻 ∈ 𝐶 )
45	41	simp3d	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) )
46	45	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) )
47	5 6 8 14	fcnre	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
48	47	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
49	42	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
50	48 49	subge0d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ↔ inf ( ran 𝐹 , ℝ , < ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
51	46 50	mpbird	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
53	48 49	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ )
54	4	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ∈ ℝ ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
55	52 53 54	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐻 ‘ 𝑡 ) = ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) )
56	51 55	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐻 ‘ 𝑡 ) )
57	56	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → 0 ≤ ( 𝐻 ‘ 𝑡 ) ) )
58	3 57	ralrimi	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 0 ≤ ( 𝐻 ‘ 𝑡 ) )
59	15	rphalfcld	⊢ ( 𝜑 → ( 𝐸 / 2 ) ∈ ℝ+ )
60	15	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
61	60	rehalfcld	⊢ ( 𝜑 → ( 𝐸 / 2 ) ∈ ℝ )
62		3re	⊢ 3 ∈ ℝ
63		3ne0	⊢ 3 ≠ 0
64	62 63	rereccli	⊢ ( 1 / 3 ) ∈ ℝ
65	64	a1i	⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℝ )
66		rphalflt	⊢ ( 𝐸 ∈ ℝ+ → ( 𝐸 / 2 ) < 𝐸 )
67	15 66	syl	⊢ ( 𝜑 → ( 𝐸 / 2 ) < 𝐸 )
68	61 60 65 67 17	lttrd	⊢ ( 𝜑 → ( 𝐸 / 2 ) < ( 1 / 3 ) )
69	19 3 5 7 6 16 8 9 27 32 12 13 44 58 59 68	stoweidlem61	⊢ ( 𝜑 → ∃ ℎ ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) )
70		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) )
71	3 70	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) )
72		rsp	⊢ ( ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) → ( 𝑡 ∈ 𝑇 → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) ) )
73	15	rpcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
74		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
75		2ne0	⊢ 2 ≠ 0
76	75	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
77	73 74 76	divcan2d	⊢ ( 𝜑 → ( 2 · ( 𝐸 / 2 ) ) = 𝐸 )
78	77	breq2d	⊢ ( 𝜑 → ( ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) ↔ ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
79	78	biimpd	⊢ ( 𝜑 → ( ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
80	72 79	sylan9r	⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) ) → ( 𝑡 ∈ 𝑇 → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
81	71 80	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) ) → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
82	81	ex	⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
83	82	reximdv	⊢ ( 𝜑 → ( ∃ ℎ ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < ( 2 · ( 𝐸 / 2 ) ) → ∃ ℎ ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
84	69 83	mpd	⊢ ( 𝜑 → ∃ ℎ ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
85		nfmpt1	⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) + inf ( ran 𝐹 , ℝ , < ) ) )
86		nfcv	⊢ Ⅎ 𝑡 ℎ
87		nfv	⊢ Ⅎ 𝑡 ℎ ∈ 𝐴
88		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸
89	87 88	nfan	⊢ Ⅎ 𝑡 ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
90	3 89	nfan	⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) )
91		eqid	⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) + inf ( ran 𝐹 , ℝ , < ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( ℎ ‘ 𝑡 ) + inf ( ran 𝐹 , ℝ , < ) ) )
92	47	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → 𝐹 : 𝑇 ⟶ ℝ )
93	42	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → inf ( ran 𝐹 , ℝ , < ) ∈ ℝ )
94	10	3adant1r	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
95	12	adantlr	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
96	9	sseld	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐴 → 𝑓 ∈ 𝐶 ) )
97	8	eleq2i	⊢ ( 𝑓 ∈ 𝐶 ↔ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
98	96 97	imbitrdi	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐴 → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) )
99		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
100		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
101	5	unieqi	⊢ ∪ 𝐾 = ∪ ( topGen ‘ ran (,) )
102	100 101	eqtr4i	⊢ ℝ = ∪ 𝐾
103	99 102	cnf	⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 : ∪ 𝐽 ⟶ ℝ )
104	98 103	syl6	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐴 → 𝑓 : ∪ 𝐽 ⟶ ℝ ) )
105		feq2	⊢ ( 𝑇 = ∪ 𝐽 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝑓 : ∪ 𝐽 ⟶ ℝ ) )
106	6 105	mp1i	⊢ ( 𝜑 → ( 𝑓 : 𝑇 ⟶ ℝ ↔ 𝑓 : ∪ 𝐽 ⟶ ℝ ) )
107	104 106	sylibrd	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐴 → 𝑓 : 𝑇 ⟶ ℝ ) )
108	2 107	ralrimi	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐴 𝑓 : 𝑇 ⟶ ℝ )
109	108	adantr	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → ∀ 𝑓 ∈ 𝐴 𝑓 : 𝑇 ⟶ ℝ )
110		simprl	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → ℎ ∈ 𝐴 )
111	55	eqcomd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) = ( 𝐻 ‘ 𝑡 ) )
112	111	oveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) = ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) )
113	112	fveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ) = ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) )
114	113	adantlr	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ) = ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) )
115		simplrr	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
116		rspa	⊢ ( ( ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
117	115 116	sylancom	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 )
118	114 117	eqbrtrd	⊢ ( ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ) < 𝐸 )
119	118	ex	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → ( 𝑡 ∈ 𝑇 → ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ) < 𝐸 ) )
120	90 119	ralrimi	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( ( 𝐹 ‘ 𝑡 ) − inf ( ran 𝐹 , ℝ , < ) ) ) ) < 𝐸 )
121	85 86 36 90 91 92 93 94 95 109 110 120	stoweidlem21	⊢ ( ( 𝜑 ∧ ( ℎ ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( ℎ ‘ 𝑡 ) − ( 𝐻 ‘ 𝑡 ) ) ) < 𝐸 ) ) → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )
122	84 121	rexlimddv	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )