Metamath Proof Explorer

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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
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 syl6ib ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐴 → 𝑓 ∈ ( 𝐽 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 ‘ ( ( 𝑓 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑡 ) ) ) < 𝐸 )