Theorem lnfnconi

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnfncon.1	⊢ 𝑇 ∈ LinFn
Assertion	lnfnconi	⊢ ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnfncon.1	⊢ 𝑇 ∈ LinFn
2		nmcfnex	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ) → ( normfn ‘ 𝑇 ) ∈ ℝ )
3	1 2	mpan	⊢ ( 𝑇 ∈ ContFn → ( normfn ‘ 𝑇 ) ∈ ℝ )
4		nmcfnlb	⊢ ( ( 𝑇 ∈ LinFn ∧ 𝑇 ∈ ContFn ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
5	1 4	mp3an1	⊢ ( ( 𝑇 ∈ ContFn ∧ 𝑦 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normfn ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
6	1	lnfnfi	⊢ 𝑇 : ℋ ⟶ ℂ
7		elcnfn	⊢ ( 𝑇 ∈ ContFn ↔ ( 𝑇 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑤 ) − ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) ) )
8	6 7	mpbiran	⊢ ( 𝑇 ∈ ContFn ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑤 ) − ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
9	6	ffvelcdmi	⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℂ )
10	9	abscld	⊢ ( 𝑦 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
11	1	lnfnsubi	⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) − ( 𝑇 ‘ 𝑥 ) ) )
12	3 5 8 10 11	lnconi	⊢ ( 𝑇 ∈ ContFn ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( abs ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )