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 𝐾 ) ↔ 𝑇 ∈ 𝐡 )