Metamath Proof Explorer

Theorem hhcnf

Description: The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhcn.1 ⊢ D = norm ℎ ∘ - ℎ
hhcn.2 ⊢ J = MetOpen ⁡ D
hhcn.4 ⊢ K = TopOpen ⁡ ℂ fld
Assertion hhcnf ⊢ ContFn = J Cn K

Proof

Step Hyp Ref Expression
1 hhcn.1 ⊢ D = norm ℎ ∘ - ℎ
2 hhcn.2 ⊢ J = MetOpen ⁡ D
3 hhcn.4 ⊢ K = TopOpen ⁡ ℂ fld
4 df-rab ⊢ t ∈ ℂ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y = t | t ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
5 df-cnfn ⊢ ContFn = t ∈ ℂ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
6 1 hilmetdval ⊢ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ x - ℎ w
7 normsub ⊢ x ∈ ℋ ∧ w ∈ ℋ → norm ℎ ⁡ x - ℎ w = norm ℎ ⁡ w - ℎ x
8 6 7 eqtrd ⊢ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ w - ℎ x
9 8 adantll ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ w - ℎ x
10 9 breq1d ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w < z ↔ norm ℎ ⁡ w - ℎ x < z
11 ffvelrn ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ → t ⁡ x ∈ ℂ
12 ffvelrn ⊢ t : ℋ ⟶ ℂ ∧ w ∈ ℋ → t ⁡ w ∈ ℂ
13 11 12 anim12dan ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x ∈ ℂ ∧ t ⁡ w ∈ ℂ
14 eqid ⊢ abs ∘ − = abs ∘ −
15 14 cnmetdval ⊢ t ⁡ x ∈ ℂ ∧ t ⁡ w ∈ ℂ → t ⁡ x abs ∘ − t ⁡ w = t ⁡ x − t ⁡ w
16 abssub ⊢ t ⁡ x ∈ ℂ ∧ t ⁡ w ∈ ℂ → t ⁡ x − t ⁡ w = t ⁡ w − t ⁡ x
17 15 16 eqtrd ⊢ t ⁡ x ∈ ℂ ∧ t ⁡ w ∈ ℂ → t ⁡ x abs ∘ − t ⁡ w = t ⁡ w − t ⁡ x
18 13 17 syl ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x abs ∘ − t ⁡ w = t ⁡ w − t ⁡ x
19 18 anassrs ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x abs ∘ − t ⁡ w = t ⁡ w − t ⁡ x
20 19 breq1d ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x abs ∘ − t ⁡ w < y ↔ t ⁡ w − t ⁡ x < y
21 10 20 imbi12d ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
22 21 ralbidva ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ → ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
23 22 rexbidv ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ → ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
24 23 ralbidv ⊢ t : ℋ ⟶ ℂ ∧ x ∈ ℋ → ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
25 24 ralbidva ⊢ t : ℋ ⟶ ℂ → ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
26 25 pm5.32i ⊢ t : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y ↔ t : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
27 1 hilxmet ⊢ D ∈ ∞Met ⁡ ℋ
28 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
29 3 cnfldtopn ⊢ K = MetOpen ⁡ abs ∘ −
30 2 29 metcn ⊢ D ∈ ∞Met ⁡ ℋ ∧ abs ∘ − ∈ ∞Met ⁡ ℂ → t ∈ J Cn K ↔ t : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y
31 27 28 30 mp2an ⊢ t ∈ J Cn K ↔ t : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x abs ∘ − t ⁡ w < y
32 cnex ⊢ ℂ ∈ V
33 ax-hilex ⊢ ℋ ∈ V
34 32 33 elmap ⊢ t ∈ ℂ ℋ ↔ t : ℋ ⟶ ℂ
35 34 anbi1i ⊢ t ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y ↔ t : ℋ ⟶ ℂ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
36 26 31 35 3bitr4i ⊢ t ∈ J Cn K ↔ t ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
37 36 abbi2i ⊢ J Cn K = t | t ∈ ℂ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → t ⁡ w − t ⁡ x < y
38 4 5 37 3eqtr4i ⊢ ContFn = J Cn K