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

Metamath Proof Explorer

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ℎ ‘ 𝑦 ) ) )