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 ffvelcdmi ⊢ ( 𝑥 ∈ ( BaseSet ‘ 𝑈 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
57 55 ffvelcdmi ⊢ ( 𝑤 ∈ ( 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 𝐾 ) ↔ 𝑇 ∈ 𝐵 )