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