# Metamath Proof Explorer

## Theorem elcnfn

Description: Property defining a continuous functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elcnfn ${⊢}{T}\in \mathrm{ContFn}↔\left({T}:ℋ⟶ℂ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{t}={T}\to {t}\left({w}\right)={T}\left({w}\right)$
2 fveq1 ${⊢}{t}={T}\to {t}\left({x}\right)={T}\left({x}\right)$
3 1 2 oveq12d ${⊢}{t}={T}\to {t}\left({w}\right)-{t}\left({x}\right)={T}\left({w}\right)-{T}\left({x}\right)$
4 3 fveq2d ${⊢}{t}={T}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|=\left|{T}\left({w}\right)-{T}\left({x}\right)\right|$
5 4 breq1d ${⊢}{t}={T}\to \left(\left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}↔\left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)$
6 5 imbi2d ${⊢}{t}={T}\to \left(\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)↔\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$
7 6 rexralbidv ${⊢}{t}={T}\to \left(\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)↔\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$
8 7 2ralbidv ${⊢}{t}={T}\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$
9 df-cnfn ${⊢}\mathrm{ContFn}=\left\{{t}\in \left({ℂ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}$
10 8 9 elrab2 ${⊢}{T}\in \mathrm{ContFn}↔\left({T}\in \left({ℂ}^{ℋ}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$
11 cnex ${⊢}ℂ\in \mathrm{V}$
12 ax-hilex ${⊢}ℋ\in \mathrm{V}$
13 11 12 elmap ${⊢}{T}\in \left({ℂ}^{ℋ}\right)↔{T}:ℋ⟶ℂ$
14 13 anbi1i ${⊢}\left({T}\in \left({ℂ}^{ℋ}\right)\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)↔\left({T}:ℋ⟶ℂ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$
15 10 14 bitri ${⊢}{T}\in \mathrm{ContFn}↔\left({T}:ℋ⟶ℂ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{T}\left({w}\right)-{T}\left({x}\right)\right|<{y}\right)\right)$