# 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$