# Metamath Proof Explorer

## Theorem lnfncon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfncon ${⊢}{T}\in \mathrm{LinFn}\to \left({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)\right)$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left({T}\in \mathrm{ContFn}↔if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\in \mathrm{ContFn}\right)$
2 fveq1 ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to {T}\left({y}\right)=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)$
3 2 fveq2d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left|{T}\left({y}\right)\right|=\left|if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)\right|$
4 3 breq1d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left(\left|{T}\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)↔\left|if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)\right)$
5 4 rexralbidv ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left(\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)↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left|if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)\right)$
6 1 5 bibi12d ${⊢}{T}=if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\to \left(\left({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)\right)↔\left(if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\in \mathrm{ContFn}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left|if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)\right)\right)$
7 0lnfn ${⊢}ℋ×\left\{0\right\}\in \mathrm{LinFn}$
8 7 elimel ${⊢}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\in \mathrm{LinFn}$
9 8 lnfnconi ${⊢}if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\in \mathrm{ContFn}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left|if\left({T}\in \mathrm{LinFn},{T},ℋ×\left\{0\right\}\right)\left({y}\right)\right|\le {x}{norm}_{ℎ}\left({y}\right)$
10 6 9 dedth ${⊢}{T}\in \mathrm{LinFn}\to \left({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)\right)$