Metamath Proof Explorer

Theorem cnfnc

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

Ref Expression
Assertion cnfnc ${⊢}\left({T}\in \mathrm{ContFn}\wedge {A}\in ℋ\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)$

Proof

Step Hyp Ref Expression
1 elcnfn ${⊢}{T}\in \mathrm{ContFn}↔\left({T}:ℋ⟶ℂ\wedge \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}\right)\right)$
2 1 simprbi ${⊢}{T}\in \mathrm{ContFn}\to \forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}\right)$
3 oveq2 ${⊢}{z}={A}\to {y}{-}_{ℎ}{z}={y}{-}_{ℎ}{A}$
4 3 fveq2d ${⊢}{z}={A}\to {norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)={norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)$
5 4 breq1d ${⊢}{z}={A}\to \left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}↔{norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\right)$
6 fveq2 ${⊢}{z}={A}\to {T}\left({z}\right)={T}\left({A}\right)$
7 6 oveq2d ${⊢}{z}={A}\to {T}\left({y}\right)-{T}\left({z}\right)={T}\left({y}\right)-{T}\left({A}\right)$
8 7 fveq2d ${⊢}{z}={A}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|=\left|{T}\left({y}\right)-{T}\left({A}\right)\right|$
9 8 breq1d ${⊢}{z}={A}\to \left(\left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}↔\left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}\right)$
10 5 9 imbi12d ${⊢}{z}={A}\to \left(\left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}\right)↔\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}\right)\right)$
11 10 rexralbidv ${⊢}{z}={A}\to \left(\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}\right)↔\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}\right)\right)$
12 breq2 ${⊢}{w}={B}\to \left(\left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}↔\left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)$
13 12 imbi2d ${⊢}{w}={B}\to \left(\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}\right)↔\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)\right)$
14 13 rexralbidv ${⊢}{w}={B}\to \left(\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{w}\right)↔\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)\right)$
15 11 14 rspc2v ${⊢}\left({A}\in ℋ\wedge {B}\in {ℝ}^{+}\right)\to \left(\forall {z}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {w}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{z}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({z}\right)\right|<{w}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)\right)$
16 2 15 syl5com ${⊢}{T}\in \mathrm{ContFn}\to \left(\left({A}\in ℋ\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)\right)$
17 16 3impib ${⊢}\left({T}\in \mathrm{ContFn}\wedge {A}\in ℋ\wedge {B}\in {ℝ}^{+}\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}{-}_{ℎ}{A}\right)<{x}\to \left|{T}\left({y}\right)-{T}\left({A}\right)\right|<{B}\right)$