Metamath Proof Explorer

Theorem htthlem

Description: Lemma for htth . The collection K , which consists of functions F ( z ) ( w ) = <. w | T ( z ) >. = <. T ( w ) | z >. for each z in the unit ball, is a collection of bounded linear functions by ipblnfi , so by the Uniform Boundedness theorem ubth , there is a uniform bound y on || F ( x ) || for all x in the unit ball. Then | T ( x ) | ^ 2 = <. T ( x ) | T ( x ) >. = F ( x ) ( T ( x ) ) <_ y | T ( x ) | , so | T ( x ) | <_ y and T is bounded. (Contributed by NM, 11-Jan-2008) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses htth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
htth.2 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
htth.3 ⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
htth.4 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
htthlem.5 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
htthlem.6 ⊢ 𝑈 ∈ CHilOLD
htthlem.7 ⊢ 𝑊 = ⟨ ⟨ + , · ⟩ , abs ⟩
htthlem.8 ⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
htthlem.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) )
htthlem.10 ⊢ 𝐹 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) )
htthlem.11 ⊢ 𝐾 = ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } )
Assertion htthlem ( 𝜑 → 𝑇 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 htth.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 htth.2 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3 htth.3 ⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
4 htth.4 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑈 )
5 htthlem.5 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
6 htthlem.6 ⊢ 𝑈 ∈ CHilOLD
7 htthlem.7 ⊢ 𝑊 = ⟨ ⟨ + , · ⟩ , abs ⟩
8 htthlem.8 ⊢ ( 𝜑 → 𝑇 ∈ 𝐿 )
9 htthlem.9 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) )
10 htthlem.10 ⊢ 𝐹 = ( 𝑧 ∈ 𝑋 ↦ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) )
11 htthlem.11 ⊢ 𝐾 = ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } )
12 6 hlnvi ⊢ 𝑈 ∈ NrmCVec
13 1 1 3 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ 𝑋 )
14 12 12 13 mp3an12 ⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ 𝑋 )
15 8 14 syl ⊢ ( 𝜑 → 𝑇 : 𝑋 ⟶ 𝑋 )
16 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 )
17 1 5 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
18 12 16 17 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
19 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑧 ) ∈ 𝑋 )
20 hlph ⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ CPreHilOLD )
21 6 20 ax-mp ⊢ 𝑈 ∈ CPreHilOLD
22 eqid ⊢ ( 𝑈 BLnOp 𝑊 ) = ( 𝑈 BLnOp 𝑊 )
23 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) )
24 1 2 21 7 22 23 ipblnfi ⊢ ( ( 𝑇 ‘ 𝑧 ) ∈ 𝑋 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) ∈ ( 𝑈 BLnOp 𝑊 ) )
25 19 24 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) ∈ ( 𝑈 BLnOp 𝑊 ) )
26 25 10 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝑈 BLnOp 𝑊 ) )
27 26 ffund ⊢ ( 𝜑 → Fun 𝐹 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Fun 𝐹 )
29 id ⊢ ( 𝑤 ∈ 𝐾 → 𝑤 ∈ 𝐾 )
30 29 11 eleqtrdi ⊢ ( 𝑤 ∈ 𝐾 → 𝑤 ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) )
31 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑤 ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) → ∃ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ( 𝐹 ‘ 𝑦 ) = 𝑤 )
32 28 30 31 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝐾 ) → ∃ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ( 𝐹 ‘ 𝑦 ) = 𝑤 )
33 32 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑤 ∈ 𝐾 → ∃ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ( 𝐹 ‘ 𝑦 ) = 𝑤 ) )
34 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑁 ‘ 𝑧 ) = ( 𝑁 ‘ 𝑦 ) )
35 34 breq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑁 ‘ 𝑧 ) ≤ 1 ↔ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) )
36 35 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) )
37 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑦 ) )
38 37 oveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) = ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
39 38 mpteq2dv ⊢ ( 𝑧 = 𝑦 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) ) )
40 39 10 1 mptfvmpt ⊢ ( 𝑦 ∈ 𝑋 → ( 𝐹 ‘ 𝑦 ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) ) )
41 40 fveq1d ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) ) ‘ 𝑥 ) )
42 oveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
43 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
44 ovex ⊢ ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ∈ V
45 42 43 44 fvmpt ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑦 ) ) ) ‘ 𝑥 ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
46 41 45 sylan9eqr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
47 46 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
48 rsp2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) )
49 9 48 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) )
50 49 impl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) )
51 50 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) )
52 47 51 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) )
53 52 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) )
54 simpl ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) → 𝑦 ∈ 𝑋 )
55 1 2 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ∈ ℂ )
56 12 55 mp3an1 ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ∈ ℂ )
57 16 54 56 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ∈ ℂ )
58 57 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) ∈ ℝ )
59 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
60 1 5 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
61 12 60 mpan ⊢ ( 𝑦 ∈ 𝑋 → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
62 61 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ )
63 59 62 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ )
64 1 5 2 21 sii ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) )
65 16 54 64 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) )
66 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → 1 ∈ ℝ )
67 1 5 nvge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
68 12 16 67 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
69 18 68 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
71 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( 𝑁 ‘ 𝑦 ) ≤ 1 )
72 lemul2a ⊢ ( ( ( ( 𝑁 ‘ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · 1 ) )
73 62 66 70 71 72 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · 1 ) )
74 59 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ )
75 74 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · 1 ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
76 73 75 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
77 58 63 59 65 76 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑇 ‘ 𝑥 ) 𝑃 𝑦 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
78 53 77 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑦 ) ≤ 1 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
79 36 78 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
80 fveq1 ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) = ( 𝑤 ‘ 𝑥 ) )
81 80 fveq2d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) ) = ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) )
82 81 breq1d ⊢ ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
83 79 82 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
84 83 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑦 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ( 𝐹 ‘ 𝑦 ) = 𝑤 → ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
85 33 84 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑤 ∈ 𝐾 → ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
86 85 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
87 brralrspcev ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 )
88 18 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 )
89 88 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 )
90 imassrn ⊢ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ⊆ ran 𝐹
91 11 90 eqsstri ⊢ 𝐾 ⊆ ran 𝐹
92 26 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑈 BLnOp 𝑊 ) )
93 91 92 sstrid ⊢ ( 𝜑 → 𝐾 ⊆ ( 𝑈 BLnOp 𝑊 ) )
94 hlobn ⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ CBan )
95 6 94 ax-mp ⊢ 𝑈 ∈ CBan
96 7 cnnv ⊢ 𝑊 ∈ NrmCVec
97 7 cnnvnm ⊢ abs = ( normCV ‘ 𝑊 )
98 eqid ⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
99 1 97 98 ubth ⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝐾 ⊆ ( 𝑈 BLnOp 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 ) )
100 95 96 99 mp3an12 ⊢ ( 𝐾 ⊆ ( 𝑈 BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 ) )
101 93 100 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( abs ‘ ( 𝑤 ‘ 𝑥 ) ) ≤ 𝑧 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 ) )
102 89 101 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 )
103 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) )
104 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑁 ‘ 𝑧 ) = ( 𝑁 ‘ 𝑥 ) )
105 104 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 ‘ 𝑧 ) ≤ 1 ↔ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) )
106 105 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) )
107 103 106 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } )
108 10 25 dmmptd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
109 108 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝑋 ) )
110 109 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom 𝐹 )
111 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
112 27 111 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
113 110 112 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
114 113 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
115 107 114 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) )
116 115 11 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )
117 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) = ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
118 117 breq1d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
119 118 rspcv ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
120 116 119 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
121 18 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
122 121 121 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
123 26 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) )
124 7 cnnvba ⊢ ℂ = ( BaseSet ‘ 𝑊 )
125 1 124 98 22 nmblore ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
126 12 96 125 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
127 123 126 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
128 127 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
129 128 121 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
130 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
131 130 121 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
132 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑥 ) )
133 132 oveq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) = ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
134 133 mpteq2dv ⊢ ( 𝑧 = 𝑥 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
135 134 10 1 mptfvmpt ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
136 135 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
137 136 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) )
138 oveq1 ⊢ ( 𝑤 = ( 𝑇 ‘ 𝑥 ) → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
139 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
140 ovex ⊢ ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) ∈ V
141 138 139 140 fvmpt ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
142 16 141 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
143 137 142 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
144 143 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
145 16 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 )
146 1 5 2 ipidsq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
147 12 145 146 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
148 144 147 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
149 148 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) )
150 resqcl ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
151 sqge0 ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → 0 ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
152 150 151 absidd ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
153 121 152 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
154 121 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ )
155 154 sqvald ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
156 149 153 155 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
157 123 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) )
158 1 5 97 98 22 12 96 nmblolbi ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
159 157 145 158 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
160 156 159 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
161 12 145 67 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
162 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
163 128 130 121 161 162 lemul1ad ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
164 122 129 131 160 163 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
165 lemul1 ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
166 165 biimprd ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
167 166 3expia ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
168 167 expdimp ⊢ ( ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
169 121 130 121 168 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
170 164 169 mpid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
171 0red ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ∈ ℝ )
172 1 124 22 blof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
173 12 96 172 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
174 123 173 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
175 174 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
176 1 124 98 nmooge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ ) → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
177 12 96 176 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
178 175 177 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
179 171 128 130 178 162 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ 𝑦 )
180 breq1 ⊢ ( 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 0 ≤ 𝑦 ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
181 179 180 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
182 0re ⊢ 0 ∈ ℝ
183 leloe ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
184 182 121 183 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
185 161 184 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
186 170 181 185 mpjaod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 )
187 186 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
188 187 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
189 120 188 syld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
190 189 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
191 190 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
192 191 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
193 192 reximdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
194 102 193 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
195 eqid ⊢ ( 𝑈 normOpOLD 𝑈 ) = ( 𝑈 normOpOLD 𝑈 )
196 1 1 5 5 195 12 12 nmobndi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑋 → ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
197 15 196 syl ⊢ ( 𝜑 → ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
198 194 197 mpbird ⊢ ( 𝜑 → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ )
199 ltpnf ⊢ ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ )
200 198 199 syl ⊢ ( 𝜑 → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ )
201 195 3 4 isblo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ ) ) )
202 12 12 201 mp2an ⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ ) )
203 8 200 202 sylanbrc ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )