Metamath Proof Explorer

Theorem cnopc

Description: Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion cnopc ⊢ T ∈ ContOp ∧ A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B

Proof

Step Hyp Ref Expression
1 elcnop ⊢ T ∈ ContOp ↔ T : ℋ ⟶ ℋ ∧ ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w
2 1 simprbi ⊢ T ∈ ContOp → ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w
3 oveq2 ⊢ z = A → y - ℎ z = y - ℎ A
4 3 fveq2d ⊢ z = A → norm ℎ ⁡ y - ℎ z = norm ℎ ⁡ y - ℎ A
5 4 breq1d ⊢ z = A → norm ℎ ⁡ y - ℎ z < x ↔ norm ℎ ⁡ y - ℎ A < x
6 fveq2 ⊢ z = A → T ⁡ z = T ⁡ A
7 6 oveq2d ⊢ z = A → T ⁡ y - ℎ T ⁡ z = T ⁡ y - ℎ T ⁡ A
8 7 fveq2d ⊢ z = A → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z = norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A
9 8 breq1d ⊢ z = A → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w ↔ norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w
10 5 9 imbi12d ⊢ z = A → norm ℎ ⁡ y - ℎ z < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w ↔ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w
11 10 rexralbidv ⊢ z = A → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w ↔ ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w
12 breq2 ⊢ w = B → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w ↔ norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B
13 12 imbi2d ⊢ w = B → norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w ↔ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B
14 13 rexralbidv ⊢ w = B → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < w ↔ ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B
15 11 14 rspc2v ⊢ A ∈ ℋ ∧ B ∈ ℝ + → ∀ z ∈ ℋ ∀ w ∈ ℝ + ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ z < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ z < w → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B
16 2 15 syl5com ⊢ T ∈ ContOp → A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B
17 16 3impib ⊢ T ∈ ContOp ∧ A ∈ ℋ ∧ B ∈ ℝ + → ∃ x ∈ ℝ + ∀ y ∈ ℋ norm ℎ ⁡ y - ℎ A < x → norm ℎ ⁡ T ⁡ y - ℎ T ⁡ A < B