# Metamath Proof Explorer

## Theorem blocni

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (Contributed by NM, 18-Dec-2007) (Revised by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses blocni.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
blocni.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
blocni.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
blocni.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
blocni.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
blocni.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
blocni.u ${⊢}{U}\in \mathrm{NrmCVec}$
blocni.w ${⊢}{W}\in \mathrm{NrmCVec}$
blocni.l ${⊢}{T}\in {L}$
Assertion blocni ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}$

### Proof

Step Hyp Ref Expression
1 blocni.8 ${⊢}{C}=\mathrm{IndMet}\left({U}\right)$
2 blocni.d ${⊢}{D}=\mathrm{IndMet}\left({W}\right)$
3 blocni.j ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
4 blocni.k ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
5 blocni.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
6 blocni.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
7 blocni.u ${⊢}{U}\in \mathrm{NrmCVec}$
8 blocni.w ${⊢}{W}\in \mathrm{NrmCVec}$
9 blocni.l ${⊢}{T}\in {L}$
10 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
11 eqid ${⊢}{0}_{\mathrm{vec}}\left({U}\right)={0}_{\mathrm{vec}}\left({U}\right)$
12 10 11 nvzcl ${⊢}{U}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)$
13 7 12 ax-mp ${⊢}{0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)$
14 10 1 imsmet ${⊢}{U}\in \mathrm{NrmCVec}\to {C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
15 7 14 ax-mp ${⊢}{C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
16 metxmet ${⊢}{C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\to {C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
17 15 16 ax-mp ${⊢}{C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)$
18 3 mopntopon ${⊢}{C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\to {J}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({U}\right)\right)$
19 17 18 ax-mp ${⊢}{J}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({U}\right)\right)$
20 19 toponunii ${⊢}\mathrm{BaseSet}\left({U}\right)=\bigcup {J}$
21 20 cncnpi ${⊢}\left({T}\in \left({J}\mathrm{Cn}{K}\right)\wedge {0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\in \left({J}\mathrm{CnP}{K}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)$
22 13 21 mpan2 ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)\to {T}\in \left({J}\mathrm{CnP}{K}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)$
23 1 2 3 4 5 6 7 8 9 10 blocnilem ${⊢}\left({0}_{\mathrm{vec}}\left({U}\right)\in \mathrm{BaseSet}\left({U}\right)\wedge {T}\in \left({J}\mathrm{CnP}{K}\right)\left({0}_{\mathrm{vec}}\left({U}\right)\right)\right)\to {T}\in {B}$
24 13 22 23 sylancr ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)\to {T}\in {B}$
25 eleq1 ${⊢}{T}={U}{0}_{\mathrm{op}}{W}\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔{U}{0}_{\mathrm{op}}{W}\in \left({J}\mathrm{Cn}{K}\right)\right)$
26 simprr ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to {y}\in {ℝ}^{+}$
27 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
28 eqid ${⊢}{U}{normOp}_{\mathrm{OLD}}{W}={U}{normOp}_{\mathrm{OLD}}{W}$
29 10 27 28 6 nmblore ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ$
30 7 8 29 mp3an12 ${⊢}{T}\in {B}\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ$
31 eqid ${⊢}{U}{0}_{\mathrm{op}}{W}={U}{0}_{\mathrm{op}}{W}$
32 28 31 5 nmlnogt0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({T}\ne {U}{0}_{\mathrm{op}}{W}↔0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\right)$
33 7 8 9 32 mp3an ${⊢}{T}\ne {U}{0}_{\mathrm{op}}{W}↔0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)$
34 33 biimpi ${⊢}{T}\ne {U}{0}_{\mathrm{op}}{W}\to 0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)$
35 30 34 anim12i ${⊢}\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\to \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge 0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\right)$
36 elrp ${⊢}\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{+}↔\left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge 0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\right)$
37 35 36 sylibr ${⊢}\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{+}$
38 37 adantr ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in {ℝ}^{+}$
39 26 38 rpdivcld ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\in {ℝ}^{+}$
40 simprl ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to {x}\in \mathrm{BaseSet}\left({U}\right)$
41 metcl ${⊢}\left({C}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{C}{w}\in ℝ$
42 15 41 mp3an1 ${⊢}\left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{C}{w}\in ℝ$
43 40 42 sylan ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {x}{C}{w}\in ℝ$
44 simplrr ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {y}\in {ℝ}^{+}$
45 44 rpred ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {y}\in ℝ$
46 35 ad2antrr ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge 0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\right)$
47 ltmuldiv2 ${⊢}\left({x}{C}{w}\in ℝ\wedge {y}\in ℝ\wedge \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge 0<\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\right)\right)\to \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)<{y}↔{x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\right)$
48 43 45 46 47 syl3anc ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)<{y}↔{x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\right)$
49 id ${⊢}\left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)$
50 49 ad2ant2r ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)$
51 10 27 1 2 28 6 7 8 blometi ${⊢}\left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)$
52 51 3expa ${⊢}\left(\left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)$
53 50 52 sylan ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)$
54 10 27 5 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)$
55 7 8 9 54 mp3an ${⊢}{T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)$
56 55 ffvelrni ${⊢}{x}\in \mathrm{BaseSet}\left({U}\right)\to {T}\left({x}\right)\in \mathrm{BaseSet}\left({W}\right)$
57 55 ffvelrni ${⊢}{w}\in \mathrm{BaseSet}\left({U}\right)\to {T}\left({w}\right)\in \mathrm{BaseSet}\left({W}\right)$
58 27 2 imsmet ${⊢}{W}\in \mathrm{NrmCVec}\to {D}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({W}\right)\right)$
59 8 58 ax-mp ${⊢}{D}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({W}\right)\right)$
60 metcl ${⊢}\left({D}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({W}\right)\right)\wedge {T}\left({x}\right)\in \mathrm{BaseSet}\left({W}\right)\wedge {T}\left({w}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\in ℝ$
61 59 60 mp3an1 ${⊢}\left({T}\left({x}\right)\in \mathrm{BaseSet}\left({W}\right)\wedge {T}\left({w}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\in ℝ$
62 56 57 61 syl2an ${⊢}\left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\in ℝ$
63 40 62 sylan ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to {T}\left({x}\right){D}{T}\left({w}\right)\in ℝ$
64 remulcl ${⊢}\left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\in ℝ\wedge {x}{C}{w}\in ℝ\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ$
65 30 42 64 syl2an ${⊢}\left({T}\in {B}\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ$
66 65 anassrs ${⊢}\left(\left({T}\in {B}\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ$
67 66 adantllr ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge {x}\in \mathrm{BaseSet}\left({U}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ$
68 67 adantlrr ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ$
69 lelttr ${⊢}\left({T}\left({x}\right){D}{T}\left({w}\right)\in ℝ\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\in ℝ\wedge {y}\in ℝ\right)\to \left(\left({T}\left({x}\right){D}{T}\left({w}\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)<{y}\right)\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
70 63 68 45 69 syl3anc ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left(\left({T}\left({x}\right){D}{T}\left({w}\right)\le \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)<{y}\right)\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
71 53 70 mpand ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left(\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)\left({x}{C}{w}\right)<{y}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
72 48 71 sylbird ${⊢}\left(\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in \mathrm{BaseSet}\left({U}\right)\right)\to \left({x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
73 72 ralrimiva ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
74 breq2 ${⊢}{z}=\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\to \left({x}{C}{w}<{z}↔{x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\right)$
75 74 rspceaimv ${⊢}\left(\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\in {ℝ}^{+}\wedge \forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<\frac{{y}}{\left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
76 39 73 75 syl2anc ${⊢}\left(\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\wedge \left({x}\in \mathrm{BaseSet}\left({U}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
77 76 ralrimivva ${⊢}\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\to \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)$
78 77 55 jctil ${⊢}\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\to \left({T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\wedge \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)\right)$
79 metxmet ${⊢}{D}\in \mathrm{Met}\left(\mathrm{BaseSet}\left({W}\right)\right)\to {D}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({W}\right)\right)$
80 59 79 ax-mp ${⊢}{D}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({W}\right)\right)$
81 3 4 metcn ${⊢}\left({C}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {D}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({W}\right)\right)\right)\to \left({T}\in \left({J}\mathrm{Cn}{K}\right)↔\left({T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\wedge \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)\right)\right)$
82 17 80 81 mp2an ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)↔\left({T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\wedge \forall {x}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in \mathrm{BaseSet}\left({U}\right)\phantom{\rule{.4em}{0ex}}\left({x}{C}{w}<{z}\to {T}\left({x}\right){D}{T}\left({w}\right)<{y}\right)\right)$
83 78 82 sylibr ${⊢}\left({T}\in {B}\wedge {T}\ne {U}{0}_{\mathrm{op}}{W}\right)\to {T}\in \left({J}\mathrm{Cn}{K}\right)$
84 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
85 10 84 31 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {U}{0}_{\mathrm{op}}{W}=\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
86 7 8 85 mp2an ${⊢}{U}{0}_{\mathrm{op}}{W}=\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
87 4 mopntopon ${⊢}{D}\in \mathrm{\infty Met}\left(\mathrm{BaseSet}\left({W}\right)\right)\to {K}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({W}\right)\right)$
88 80 87 ax-mp ${⊢}{K}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({W}\right)\right)$
89 27 84 nvzcl ${⊢}{W}\in \mathrm{NrmCVec}\to {0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{BaseSet}\left({W}\right)$
90 8 89 ax-mp ${⊢}{0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{BaseSet}\left({W}\right)$
91 cnconst2 ${⊢}\left({J}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({U}\right)\right)\wedge {K}\in \mathrm{TopOn}\left(\mathrm{BaseSet}\left({W}\right)\right)\wedge {0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{BaseSet}\left({W}\right)\right)\to \mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\in \left({J}\mathrm{Cn}{K}\right)$
92 19 88 90 91 mp3an ${⊢}\mathrm{BaseSet}\left({U}\right)×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\in \left({J}\mathrm{Cn}{K}\right)$
93 86 92 eqeltri ${⊢}{U}{0}_{\mathrm{op}}{W}\in \left({J}\mathrm{Cn}{K}\right)$
94 93 a1i ${⊢}{T}\in {B}\to {U}{0}_{\mathrm{op}}{W}\in \left({J}\mathrm{Cn}{K}\right)$
95 25 83 94 pm2.61ne ${⊢}{T}\in {B}\to {T}\in \left({J}\mathrm{Cn}{K}\right)$
96 24 95 impbii ${⊢}{T}\in \left({J}\mathrm{Cn}{K}\right)↔{T}\in {B}$