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 𝐶 = ( IndMet ‘ 𝑈 )
blocni.d 𝐷 = ( IndMet ‘ 𝑊 )
blocni.j 𝐽 = ( MetOpen ‘ 𝐶 )
blocni.k 𝐾 = ( MetOpen ‘ 𝐷 )
blocni.4 𝐿 = ( 𝑈 LnOp 𝑊 )
blocni.5 𝐵 = ( 𝑈 BLnOp 𝑊 )
blocni.u 𝑈 ∈ NrmCVec
blocni.w 𝑊 ∈ NrmCVec
blocni.l 𝑇𝐿
Assertion blocni ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇𝐵 )

Proof

Step Hyp Ref Expression
1 blocni.8 𝐶 = ( IndMet ‘ 𝑈 )
2 blocni.d 𝐷 = ( IndMet ‘ 𝑊 )
3 blocni.j 𝐽 = ( MetOpen ‘ 𝐶 )
4 blocni.k 𝐾 = ( MetOpen ‘ 𝐷 )
5 blocni.4 𝐿 = ( 𝑈 LnOp 𝑊 )
6 blocni.5 𝐵 = ( 𝑈 BLnOp 𝑊 )
7 blocni.u 𝑈 ∈ NrmCVec
8 blocni.w 𝑊 ∈ NrmCVec
9 blocni.l 𝑇𝐿
10 eqid ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
11 eqid ( 0vec𝑈 ) = ( 0vec𝑈 )
12 10 11 nvzcl ( 𝑈 ∈ NrmCVec → ( 0vec𝑈 ) ∈ ( BaseSet ‘ 𝑈 ) )
13 7 12 ax-mp ( 0vec𝑈 ) ∈ ( BaseSet ‘ 𝑈 )
14 10 1 imsmet ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) )
15 7 14 ax-mp 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) )
16 metxmet ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) → 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) )
17 15 16 ax-mp 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) )
18 3 mopntopon ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) )
19 17 18 ax-mp 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) )
20 19 toponunii ( BaseSet ‘ 𝑈 ) = 𝐽
21 20 cncnpi ( ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 0vec𝑈 ) ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( 0vec𝑈 ) ) )
22 13 21 mpan2 ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) → 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( 0vec𝑈 ) ) )
23 1 2 3 4 5 6 7 8 9 10 blocnilem ( ( ( 0vec𝑈 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑇 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ ( 0vec𝑈 ) ) ) → 𝑇𝐵 )
24 13 22 23 sylancr ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) → 𝑇𝐵 )
25 eleq1 ( 𝑇 = ( 𝑈 0op 𝑊 ) → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑈 0op 𝑊 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
26 simprr ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ+ )
27 eqid ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
28 eqid ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
29 10 27 28 6 nmblore ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐵 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
30 7 8 29 mp3an12 ( 𝑇𝐵 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
31 eqid ( 𝑈 0op 𝑊 ) = ( 𝑈 0op 𝑊 )
32 28 31 5 nmlnogt0 ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) → ( 𝑇 ≠ ( 𝑈 0op 𝑊 ) ↔ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) )
33 7 8 9 32 mp3an ( 𝑇 ≠ ( 𝑈 0op 𝑊 ) ↔ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) )
34 33 biimpi ( 𝑇 ≠ ( 𝑈 0op 𝑊 ) → 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) )
35 30 34 anim12i ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) )
36 elrp ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ+ ↔ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) )
37 35 36 sylibr ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ+ )
38 37 adantr ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ+ )
39 26 38 rpdivcld ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ∈ ℝ+ )
40 simprl ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ ( BaseSet ‘ 𝑈 ) )
41 metcl ( ( 𝐶 ∈ ( Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ )
42 15 41 mp3an1 ( ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ )
43 40 42 sylan ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 𝐶 𝑤 ) ∈ ℝ )
44 simplrr ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑦 ∈ ℝ+ )
45 44 rpred ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → 𝑦 ∈ ℝ )
46 35 ad2antrr ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) )
47 ltmuldiv2 ( ( ( 𝑥 𝐶 𝑤 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ 0 < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ) → ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) < 𝑦 ↔ ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ) )
48 43 45 46 47 syl3anc ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) < 𝑦 ↔ ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ) )
49 id ( ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) )
50 49 ad2ant2r ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) )
51 10 27 1 2 28 6 7 8 blometi ( ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) )
52 51 3expa ( ( ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) )
53 50 52 sylan ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) )
54 10 27 5 lnof ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿 ) → 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
55 7 8 9 54 mp3an 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 )
56 55 ffvelrni ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑇𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
57 55 ffvelrni ( 𝑤 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑇𝑤 ) ∈ ( BaseSet ‘ 𝑊 ) )
58 27 2 imsmet ( 𝑊 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ ( BaseSet ‘ 𝑊 ) ) )
59 8 58 ax-mp 𝐷 ∈ ( Met ‘ ( BaseSet ‘ 𝑊 ) )
60 metcl ( ( 𝐷 ∈ ( Met ‘ ( BaseSet ‘ 𝑊 ) ) ∧ ( 𝑇𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑇𝑤 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ∈ ℝ )
61 59 60 mp3an1 ( ( ( 𝑇𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑇𝑤 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ∈ ℝ )
62 56 57 61 syl2an ( ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ∈ ℝ )
63 40 62 sylan ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ∈ ℝ )
64 remulcl ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ ( 𝑥 𝐶 𝑤 ) ∈ ℝ ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
65 30 42 64 syl2an ( ( 𝑇𝐵 ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
66 65 anassrs ( ( ( 𝑇𝐵𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
67 66 adantllr ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
68 67 adantlrr ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ )
69 lelttr ( ( ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ∈ ℝ ∧ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∧ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) < 𝑦 ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
70 63 68 45 69 syl3anc ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) ∧ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) < 𝑦 ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
71 53 70 mpand ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑥 𝐶 𝑤 ) ) < 𝑦 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
72 48 71 sylbird ( ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) ∧ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
73 72 ralrimiva ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
74 breq2 ( 𝑧 = ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) → ( ( 𝑥 𝐶 𝑤 ) < 𝑧 ↔ ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ) )
75 74 rspceaimv ( ( ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) ∈ ℝ+ ∧ ∀ 𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < ( 𝑦 / ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ) → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
76 39 73 75 syl2anc ( ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) ∧ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
77 76 ralrimivva ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) → ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) )
78 77 55 jctil ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) → ( 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) ) )
79 metxmet ( 𝐷 ∈ ( Met ‘ ( BaseSet ‘ 𝑊 ) ) → 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) )
80 59 79 ax-mp 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) )
81 3 4 metcn ( ( 𝐶 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) ) → ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) ) ) )
82 17 80 81 mp2an ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑇 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ( BaseSet ‘ 𝑈 ) ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝑇𝑥 ) 𝐷 ( 𝑇𝑤 ) ) < 𝑦 ) ) )
83 78 82 sylibr ( ( 𝑇𝐵𝑇 ≠ ( 𝑈 0op 𝑊 ) ) → 𝑇 ∈ ( 𝐽 Cn 𝐾 ) )
84 eqid ( 0vec𝑊 ) = ( 0vec𝑊 )
85 10 84 31 0ofval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 0op 𝑊 ) = ( ( BaseSet ‘ 𝑈 ) × { ( 0vec𝑊 ) } ) )
86 7 8 85 mp2an ( 𝑈 0op 𝑊 ) = ( ( BaseSet ‘ 𝑈 ) × { ( 0vec𝑊 ) } )
87 4 mopntopon ( 𝐷 ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) → 𝐾 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) )
88 80 87 ax-mp 𝐾 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) )
89 27 84 nvzcl ( 𝑊 ∈ NrmCVec → ( 0vec𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) )
90 8 89 ax-mp ( 0vec𝑊 ) ∈ ( BaseSet ‘ 𝑊 )
91 cnconst2 ( ( 𝐽 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑈 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) ∧ ( 0vec𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( BaseSet ‘ 𝑈 ) × { ( 0vec𝑊 ) } ) ∈ ( 𝐽 Cn 𝐾 ) )
92 19 88 90 91 mp3an ( ( BaseSet ‘ 𝑈 ) × { ( 0vec𝑊 ) } ) ∈ ( 𝐽 Cn 𝐾 )
93 86 92 eqeltri ( 𝑈 0op 𝑊 ) ∈ ( 𝐽 Cn 𝐾 )
94 93 a1i ( 𝑇𝐵 → ( 𝑈 0op 𝑊 ) ∈ ( 𝐽 Cn 𝐾 ) )
95 25 83 94 pm2.61ne ( 𝑇𝐵𝑇 ∈ ( 𝐽 Cn 𝐾 ) )
96 24 95 impbii ( 𝑇 ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝑇𝐵 )