# 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}\in \mathrm{LinOp}$
Assertion lnopconi ${⊢}{T}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$

### Proof

Step Hyp Ref Expression
1 lnopcon.1 ${⊢}{T}\in \mathrm{LinOp}$
2 nmcopex ${⊢}\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\right)\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
3 1 2 mpan ${⊢}{T}\in \mathrm{ContOp}\to {norm}_{\mathrm{op}}\left({T}\right)\in ℝ$
4 nmcoplb ${⊢}\left({T}\in \mathrm{LinOp}\wedge {T}\in \mathrm{ContOp}\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)$
5 1 4 mp3an1 ${⊢}\left({T}\in \mathrm{ContOp}\wedge {y}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({y}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right){norm}_{ℎ}\left({y}\right)$
6 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
7 elcnop ${⊢}{T}\in \mathrm{ContOp}↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {norm}_{ℎ}\left({T}\left({w}\right){-}_{ℎ}{T}\left({x}\right)\right)<{z}\right)\right)$
8 6 7 mpbiran ${⊢}{T}\in \mathrm{ContOp}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{y}\to {norm}_{ℎ}\left({T}\left({w}\right){-}_{ℎ}{T}\left({x}\right)\right)<{z}\right)$
9 6 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℋ$
10 normcl ${⊢}{T}\left({y}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({y}\right)\right)\in ℝ$
11 9 10 syl ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left({T}\left({y}\right)\right)\in ℝ$
12 1 lnopsubi ${⊢}\left({w}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right){-}_{ℎ}{T}\left({x}\right)$
13 3 5 8 11 12 lnconi ${⊢}{T}\in \mathrm{ContOp}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)\le {x}{norm}_{ℎ}\left({y}\right)$