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 ( ( 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elcnop ( 𝑇 ∈ ContOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑧 ∈ ℋ ∀ 𝑤 ∈ ℝ+𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ) ) )
2 1 simprbi ( 𝑇 ∈ ContOp → ∀ 𝑧 ∈ ℋ ∀ 𝑤 ∈ ℝ+𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ) )
3 oveq2 ( 𝑧 = 𝐴 → ( 𝑦 𝑧 ) = ( 𝑦 𝐴 ) )
4 3 fveq2d ( 𝑧 = 𝐴 → ( norm ‘ ( 𝑦 𝑧 ) ) = ( norm ‘ ( 𝑦 𝐴 ) ) )
5 4 breq1d ( 𝑧 = 𝐴 → ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 ↔ ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 ) )
6 fveq2 ( 𝑧 = 𝐴 → ( 𝑇𝑧 ) = ( 𝑇𝐴 ) )
7 6 oveq2d ( 𝑧 = 𝐴 → ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) = ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) )
8 7 fveq2d ( 𝑧 = 𝐴 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) = ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) )
9 8 breq1d ( 𝑧 = 𝐴 → ( ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ↔ ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ) )
10 5 9 imbi12d ( 𝑧 = 𝐴 → ( ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ) ↔ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ) ) )
11 10 rexralbidv ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ) ↔ ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ) ) )
12 breq2 ( 𝑤 = 𝐵 → ( ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ↔ ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) )
13 12 imbi2d ( 𝑤 = 𝐵 → ( ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ) ↔ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) ) )
14 13 rexralbidv ( 𝑤 = 𝐵 → ( ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝑤 ) ↔ ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) ) )
15 11 14 rspc2v ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ℋ ∀ 𝑤 ∈ ℝ+𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝑧 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝑧 ) ) ) < 𝑤 ) → ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) ) )
16 2 15 syl5com ( 𝑇 ∈ ContOp → ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) ) )
17 16 3impib ( ( 𝑇 ∈ ContOp ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+𝑦 ∈ ℋ ( ( norm ‘ ( 𝑦 𝐴 ) ) < 𝑥 → ( norm ‘ ( ( 𝑇𝑦 ) − ( 𝑇𝐴 ) ) ) < 𝐵 ) )