Metamath Proof Explorer

Theorem hhcno

Description: The continuous operators 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
Assertion hhcno ⊢ ContOp = J Cn J

Proof

Step Hyp Ref Expression
1 hhcn.1 ⊢ D = norm ℎ ∘ - ℎ
2 hhcn.2 ⊢ J = MetOpen ⁡ D
3 df-rab ⊢ t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y = t | t ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
4 df-cnop ⊢ ContOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
5 1 hilmetdval ⊢ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ x - ℎ w
6 normsub ⊢ x ∈ ℋ ∧ w ∈ ℋ → norm ℎ ⁡ x - ℎ w = norm ℎ ⁡ w - ℎ x
7 5 6 eqtrd ⊢ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ w - ℎ x
8 7 adantll ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w = norm ℎ ⁡ w - ℎ x
9 8 breq1d ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w < z ↔ norm ℎ ⁡ w - ℎ x < z
10 ffvelcdm ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ → t ⁡ x ∈ ℋ
11 ffvelcdm ⊢ t : ℋ ⟶ ℋ ∧ w ∈ ℋ → t ⁡ w ∈ ℋ
12 10 11 anim12dan ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x ∈ ℋ ∧ t ⁡ w ∈ ℋ
13 1 hilmetdval ⊢ t ⁡ x ∈ ℋ ∧ t ⁡ w ∈ ℋ → t ⁡ x D t ⁡ w = norm ℎ ⁡ t ⁡ x - ℎ t ⁡ w
14 normsub ⊢ t ⁡ x ∈ ℋ ∧ t ⁡ w ∈ ℋ → norm ℎ ⁡ t ⁡ x - ℎ t ⁡ w = norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x
15 13 14 eqtrd ⊢ t ⁡ x ∈ ℋ ∧ t ⁡ w ∈ ℋ → t ⁡ x D t ⁡ w = norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x
16 12 15 syl ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x D t ⁡ w = norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x
17 16 anassrs ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x D t ⁡ w = norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x
18 17 breq1d ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → t ⁡ x D t ⁡ w < y ↔ norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
19 9 18 imbi12d ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ ∧ w ∈ ℋ → x D w < z → t ⁡ x D t ⁡ w < y ↔ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
20 19 ralbidva ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ → ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y ↔ ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
21 20 rexbidv ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ → ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y ↔ ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
22 21 ralbidv ⊢ t : ℋ ⟶ ℋ ∧ x ∈ ℋ → ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y ↔ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
23 22 ralbidva ⊢ t : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y ↔ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
24 23 pm5.32i ⊢ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y ↔ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
25 1 hilxmet ⊢ D ∈ ∞Met ⁡ ℋ
26 2 2 metcn ⊢ D ∈ ∞Met ⁡ ℋ ∧ D ∈ ∞Met ⁡ ℋ → t ∈ J Cn J ↔ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y
27 25 25 26 mp2an ⊢ t ∈ J Cn J ↔ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ x D w < z → t ⁡ x D t ⁡ w < y
28 ax-hilex ⊢ ℋ ∈ V
29 28 28 elmap ⊢ t ∈ ℋ ℋ ↔ t : ℋ ⟶ ℋ
30 29 anbi1i ⊢ t ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y ↔ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
31 24 27 30 3bitr4i ⊢ t ∈ J Cn J ↔ t ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
32 31 eqabi ⊢ J Cn J = t | t ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
33 3 4 32 3eqtr4i ⊢ ContOp = J Cn J