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

### Proof

Step Hyp Ref Expression
1 lnfncon.1 ${⊢}{T}\in \mathrm{LinFn}$
2 nmcfnex ${⊢}\left({T}\in \mathrm{LinFn}\wedge {T}\in \mathrm{ContFn}\right)\to {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ$
3 1 2 mpan ${⊢}{T}\in \mathrm{ContFn}\to {norm}_{\mathrm{fn}}\left({T}\right)\in ℝ$
4 nmcfnlb ${⊢}\left({T}\in \mathrm{LinFn}\wedge {T}\in \mathrm{ContFn}\wedge {y}\in ℋ\right)\to \left|{T}\left({y}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({y}\right)$
5 1 4 mp3an1 ${⊢}\left({T}\in \mathrm{ContFn}\wedge {y}\in ℋ\right)\to \left|{T}\left({y}\right)\right|\le {norm}_{\mathrm{fn}}\left({T}\right){norm}_{ℎ}\left({y}\right)$
6 1 lnfnfi ${⊢}{T}:ℋ⟶ℂ$
7 elcnfn ${⊢}{T}\in \mathrm{ContFn}↔\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 \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{z}\right)\right)$
8 6 7 mpbiran ${⊢}{T}\in \mathrm{ContFn}↔\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 \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{z}\right)$
9 6 ffvelrni ${⊢}{y}\in ℋ\to {T}\left({y}\right)\in ℂ$
10 9 abscld ${⊢}{y}\in ℋ\to \left|{T}\left({y}\right)\right|\in ℝ$
11 1 lnfnsubi ${⊢}\left({w}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({w}{-}_{ℎ}{x}\right)={T}\left({w}\right)-{T}\left({x}\right)$
12 3 5 8 10 11 lnconi ${⊢}{T}\in \mathrm{ContFn}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left|{T}\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)$