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 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑁 ‘ 𝑧 ) = ( 𝑁 ‘ 𝑥 ) )
104 103 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 ‘ 𝑧 ) ≤ 1 ↔ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) )
105 104 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) )
106 105 bilanri ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } )
107 10 25 dmmptd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
108 107 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝑋 ) )
109 108 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom 𝐹 )
110 funfvima ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
111 27 110 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
112 109 111 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
113 112 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝑥 ∈ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) ) )
114 106 113 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ { 𝑧 ∈ 𝑋 ∣ ( 𝑁 ‘ 𝑧 ) ≤ 1 } ) )
115 114 11 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )
116 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) = ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
117 116 breq1d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 ↔ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
118 117 rspcv ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
119 115 118 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) )
120 18 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
121 120 120 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
122 26 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) )
123 7 cnnvba ⊢ ℂ = ( BaseSet ‘ 𝑊 )
124 1 123 98 22 nmblore ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
125 12 96 124 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
126 122 125 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
127 126 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
128 127 120 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
129 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
130 129 120 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ∈ ℝ )
131 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ 𝑥 ) )
132 131 oveq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) = ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
133 132 mpteq2dv ⊢ ( 𝑧 = 𝑥 → ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑧 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
134 133 10 1 mptfvmpt ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
135 134 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) )
136 135 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) )
137 oveq1 ⊢ ( 𝑤 = ( 𝑇 ‘ 𝑥 ) → ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
138 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
139 ovex ⊢ ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) ∈ V
140 137 138 139 fvmpt ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
141 16 140 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 𝑃 ( 𝑇 ‘ 𝑥 ) ) ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
142 136 141 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
143 142 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) )
144 16 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 )
145 1 5 2 ipidsq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
146 12 144 145 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑇 ‘ 𝑥 ) 𝑃 ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
147 143 146 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
148 147 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) )
149 resqcl ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
150 sqge0 ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → 0 ≤ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
151 149 150 absidd ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ → ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
152 120 151 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) )
153 120 recnd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℂ )
154 153 sqvald ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
155 148 152 154 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
156 122 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) )
157 1 5 97 98 22 12 96 nmblolbi ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ∧ ( 𝑇 ‘ 𝑥 ) ∈ 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
158 156 144 157 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
159 155 158 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
160 12 144 67 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) )
161 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 )
162 127 129 120 160 161 lemul1ad ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
163 121 128 130 159 162 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
164 lemul1 ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ↔ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
165 164 biimprd ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
166 165 3expia ⊢ ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
167 166 expdimp ⊢ ( ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
168 120 129 120 167 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ≤ ( 𝑦 · ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
169 163 168 mpid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
170 0red ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ∈ ℝ )
171 1 123 22 blof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
172 12 96 171 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑈 BLnOp 𝑊 ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
173 122 172 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
174 173 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ )
175 1 123 98 nmooge0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ ) → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
176 12 96 175 mp3an12 ⊢ ( ( 𝐹 ‘ 𝑥 ) : 𝑋 ⟶ ℂ → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
177 174 176 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
178 170 127 129 177 161 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → 0 ≤ 𝑦 )
179 breq1 ⊢ ( 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 0 ≤ 𝑦 ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
180 178 179 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
181 0re ⊢ 0 ∈ ℝ
182 leloe ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → ( 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
183 181 120 182 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 ≤ ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) )
184 160 183 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 0 < ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ∨ 0 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
185 169 180 184 mpjaod ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 )
186 185 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
187 186 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
188 119 187 syld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) ≤ 1 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
189 188 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
190 189 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
191 190 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
192 191 reximdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ 𝐾 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑤 ) ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
193 102 192 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) )
194 eqid ⊢ ( 𝑈 normOpOLD 𝑈 ) = ( 𝑈 normOpOLD 𝑈 )
195 1 1 5 5 194 12 12 nmobndi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑋 → ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
196 15 195 syl ⊢ ( 𝜑 → ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝑦 ) ) )
197 193 196 mpbird ⊢ ( 𝜑 → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ )
198 ltpnf ⊢ ( ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) ∈ ℝ → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ )
199 197 198 syl ⊢ ( 𝜑 → ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ )
200 194 3 4 isblo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ ) ) )
201 12 12 200 mp2an ⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑈 ) ‘ 𝑇 ) < +∞ ) )
202 8 199 201 sylanbrc ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )