This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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ℎ ‘ ( ( 𝑇 ‘ 𝑦 ) −ℎ ( 𝑇 ‘ 𝐴 ) ) ) < 𝐵 ) )