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

Metamath Proof Explorer

Theorem lnopconi

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

Ref Expression
Hypothesis lnopcon.1 ⊢ 𝑇 ∈ LinOp
Assertion lnopconi ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 lnopcon.1 ⊢ 𝑇 ∈ LinOp
2 nmcopex ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ) → ( normop ‘ 𝑇 ) ∈ ℝ )
3 1 2 mpan ⊢ ( 𝑇 ∈ ContOp → ( normop ‘ 𝑇 ) ∈ ℝ )
4 nmcoplb ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑇 ∈ ContOp ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
5 1 4 mp3an1 ⊢ ( ( 𝑇 ∈ ContOp ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑦 ) ) )
6 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
7 elcnop ⊢ ( 𝑇 ∈ ContOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) ) )
8 6 7 mpbiran ⊢ ( 𝑇 ∈ ContOp ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑦 → ( normℎ ‘ ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) < 𝑧 ) )
9 6 ffvelcdmi ⊢ ( 𝑦 ∈ ℋ → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
10 normcl ⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
11 9 10 syl ⊢ ( 𝑦 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
12 1 lnopsubi ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑤 −ℎ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑤 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
13 3 5 8 11 12 lnconi ⊢ ( 𝑇 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑦 ) ) )