Theorem cnfnc

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

	Ref	Expression
Assertion	cnfnc	⊢ ( ( 𝑇 ∈ ContFn ∧ 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ ℋ ( ( normℎ ‘ ( 𝑦 −ℎ 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝑇 ‘ 𝑦 ) − ( 𝑇 ‘ 𝐴 ) ) ) < 𝐵 ) )

Proof

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