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 ⊢ T ∈ LinOp
Assertion lnopconi ⊢ T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y

Proof

Step Hyp Ref Expression
1 lnopcon.1 ⊢ T ∈ LinOp
2 nmcopex ⊢ T ∈ LinOp ∧ T ∈ ContOp → norm op ⁡ T ∈ ℝ
3 1 2 mpan ⊢ T ∈ ContOp → norm op ⁡ T ∈ ℝ
4 nmcoplb ⊢ T ∈ LinOp ∧ T ∈ ContOp ∧ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
5 1 4 mp3an1 ⊢ T ∈ ContOp ∧ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ≤ norm op ⁡ T ⁢ norm ℎ ⁡ y
6 1 lnopfi ⊢ T : ℋ ⟶ ℋ
7 elcnop ⊢ T ∈ ContOp ↔ T : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ z ∈ ℝ + ∃ y ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < y → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < z
8 6 7 mpbiran ⊢ T ∈ ContOp ↔ ∀ x ∈ ℋ ∀ z ∈ ℝ + ∃ y ∈ ℝ + ∀ w ∈ ℋ norm ℎ ⁡ w - ℎ x < y → norm ℎ ⁡ T ⁡ w - ℎ T ⁡ x < z
9 6 ffvelrni ⊢ y ∈ ℋ → T ⁡ y ∈ ℋ
10 normcl ⊢ T ⁡ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ∈ ℝ
11 9 10 syl ⊢ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ∈ ℝ
12 1 lnopsubi ⊢ w ∈ ℋ ∧ x ∈ ℋ → T ⁡ w - ℎ x = T ⁡ w - ℎ T ⁡ x
13 3 5 8 11 12 lnconi ⊢ T ∈ ContOp ↔ ∃ x ∈ ℝ ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y ≤ x ⁢ norm ℎ ⁡ y