Metamath Proof Explorer

Theorem elcnop

Description: Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elcnop ⊢ T ∈ ContOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ t = T → t ⁡ w = T ⁡ w
2 fveq1 ⊢ t = T → t ⁡ x = T ⁡ x
3 1 2 oveq12d ⊢ t = T → t ⁡ w - ℎ t ⁡ x = T ⁡ w - ℎ T ⁡ x
4 3 fveq2d ⊢ t = T → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x = norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x
5 4 breq1d ⊢ t = T → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y ↔ norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y
6 5 imbi2d ⊢ t = T → norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y ↔ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y
7 6 rexralbidv ⊢ t = T → ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y ↔ ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y
8 7 2ralbidv ⊢ t = T → ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y ↔ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y
9 df-cnop ⊢ ContOp = t ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ t ⁡ w - ℎ t ⁡ x < y
10 8 9 elrab2 ⊢ T ∈ ContOp ↔ T ∈ ℋ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y
11 ax-hilex ⊢ ℋ ∈ V
12 11 11 elmap ⊢ T ∈ ℋ ℋ ↔ T : ℋ ⟶ ℋ
13 12 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
14 10 13 bitri ⊢ T ∈ ContOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℝ + ∃ z ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < z → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < y