Metamath Proof Explorer


Theorem ubthlem2

Description: Lemma for ubth . Given that there is a closed ball B ( P , R ) in AK , for any x e. B ( 0 , 1 ) , we have P + R x. x e. B ( P , R ) and P e. B ( P , R ) , so both of these have norm ( t ( z ) ) <_ K and so norm ( t ( x ) ) <_ ( norm ( t ( P ) ) + norm ( t ( P + R x. x ) ) ) / R <_ ( K + K ) / R , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 𝑋 = ( BaseSet ‘ 𝑈 )
ubth.2 𝑁 = ( normCV𝑊 )
ubthlem.3 𝐷 = ( IndMet ‘ 𝑈 )
ubthlem.4 𝐽 = ( MetOpen ‘ 𝐷 )
ubthlem.5 𝑈 ∈ CBan
ubthlem.6 𝑊 ∈ NrmCVec
ubthlem.7 ( 𝜑𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
ubthlem.8 ( 𝜑 → ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 )
ubthlem.9 𝐴 = ( 𝑘 ∈ ℕ ↦ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝑘 } )
ubthlem.10 ( 𝜑𝐾 ∈ ℕ )
ubthlem.11 ( 𝜑𝑃𝑋 )
ubthlem.12 ( 𝜑𝑅 ∈ ℝ+ )
ubthlem.13 ( 𝜑 → { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ⊆ ( 𝐴𝐾 ) )
Assertion ubthlem2 ( 𝜑 → ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )

Proof

Step Hyp Ref Expression
1 ubth.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 ubth.2 𝑁 = ( normCV𝑊 )
3 ubthlem.3 𝐷 = ( IndMet ‘ 𝑈 )
4 ubthlem.4 𝐽 = ( MetOpen ‘ 𝐷 )
5 ubthlem.5 𝑈 ∈ CBan
6 ubthlem.6 𝑊 ∈ NrmCVec
7 ubthlem.7 ( 𝜑𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
8 ubthlem.8 ( 𝜑 → ∀ 𝑥𝑋𝑐 ∈ ℝ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ 𝑐 )
9 ubthlem.9 𝐴 = ( 𝑘 ∈ ℕ ↦ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝑘 } )
10 ubthlem.10 ( 𝜑𝐾 ∈ ℕ )
11 ubthlem.11 ( 𝜑𝑃𝑋 )
12 ubthlem.12 ( 𝜑𝑅 ∈ ℝ+ )
13 ubthlem.13 ( 𝜑 → { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ⊆ ( 𝐴𝐾 ) )
14 10 nnrpd ( 𝜑𝐾 ∈ ℝ+ )
15 14 14 rpaddcld ( 𝜑 → ( 𝐾 + 𝐾 ) ∈ ℝ+ )
16 15 12 rpdivcld ( 𝜑 → ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ+ )
17 16 rpred ( 𝜑 → ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ )
18 oveq2 ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( 𝑃 𝐷 𝑧 ) = ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) )
19 18 breq1d ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ↔ ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ≤ 𝑅 ) )
20 eleq1 ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( 𝑧 ∈ ( 𝐴𝐾 ) ↔ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ) )
21 19 20 imbi12d ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅𝑧 ∈ ( 𝐴𝐾 ) ) ↔ ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ≤ 𝑅 → ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ) ) )
22 rabss ( { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ⊆ ( 𝐴𝐾 ) ↔ ∀ 𝑧𝑋 ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅𝑧 ∈ ( 𝐴𝐾 ) ) )
23 13 22 sylib ( 𝜑 → ∀ 𝑧𝑋 ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅𝑧 ∈ ( 𝐴𝐾 ) ) )
24 23 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ∀ 𝑧𝑋 ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅𝑧 ∈ ( 𝐴𝐾 ) ) )
25 bnnv ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
26 5 25 ax-mp 𝑈 ∈ NrmCVec
27 26 a1i ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑈 ∈ NrmCVec )
28 11 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑃𝑋 )
29 12 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑅 ∈ ℝ+ )
30 29 rpcnd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑅 ∈ ℂ )
31 simpr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
32 eqid ( ·𝑠OLD𝑈 ) = ( ·𝑠OLD𝑈 )
33 1 32 nvscl ( ( 𝑈 ∈ NrmCVec ∧ 𝑅 ∈ ℂ ∧ 𝑥𝑋 ) → ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ∈ 𝑋 )
34 27 30 31 33 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ∈ 𝑋 )
35 eqid ( +𝑣𝑈 ) = ( +𝑣𝑈 )
36 1 35 nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ∈ 𝑋 ) → ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 )
37 27 28 34 36 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 )
38 21 24 37 rspcdva ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ≤ 𝑅 → ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ) )
39 1 3 cbncms ( 𝑈 ∈ CBan → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
40 5 39 ax-mp 𝐷 ∈ ( CMet ‘ 𝑋 )
41 cmetmet ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
42 metxmet ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
43 40 41 42 mp2b 𝐷 ∈ ( ∞Met ‘ 𝑋 )
44 43 a1i ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
45 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ) → ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) = ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) 𝐷 𝑃 ) )
46 44 28 37 45 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) = ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) 𝐷 𝑃 ) )
47 eqid ( −𝑣𝑈 ) = ( −𝑣𝑈 )
48 eqid ( normCV𝑈 ) = ( normCV𝑈 )
49 1 47 48 3 imsdval ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋𝑃𝑋 ) → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) 𝐷 𝑃 ) = ( ( normCV𝑈 ) ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) )
50 27 37 28 49 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) 𝐷 𝑃 ) = ( ( normCV𝑈 ) ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) )
51 1 35 47 nvpncan2 ( ( 𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ∈ 𝑋 ) → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) = ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) )
52 27 28 34 51 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) = ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) )
53 52 fveq2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( normCV𝑈 ) ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) = ( ( normCV𝑈 ) ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) )
54 46 50 53 3eqtrd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) = ( ( normCV𝑈 ) ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) )
55 29 rprege0d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
56 1 32 48 nvsge0 ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ 𝑥𝑋 ) → ( ( normCV𝑈 ) ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) = ( 𝑅 · ( ( normCV𝑈 ) ‘ 𝑥 ) ) )
57 27 55 31 56 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( normCV𝑈 ) ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) = ( 𝑅 · ( ( normCV𝑈 ) ‘ 𝑥 ) ) )
58 54 57 eqtrd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) = ( 𝑅 · ( ( normCV𝑈 ) ‘ 𝑥 ) ) )
59 30 mulid1d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑅 · 1 ) = 𝑅 )
60 59 eqcomd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑅 = ( 𝑅 · 1 ) )
61 58 60 breq12d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ≤ 𝑅 ↔ ( 𝑅 · ( ( normCV𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑅 · 1 ) ) )
62 1 48 nvcl ( ( 𝑈 ∈ NrmCVec ∧ 𝑥𝑋 ) → ( ( normCV𝑈 ) ‘ 𝑥 ) ∈ ℝ )
63 26 62 mpan ( 𝑥𝑋 → ( ( normCV𝑈 ) ‘ 𝑥 ) ∈ ℝ )
64 63 adantl ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( normCV𝑈 ) ‘ 𝑥 ) ∈ ℝ )
65 1red ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 1 ∈ ℝ )
66 64 65 29 lemul2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 ↔ ( 𝑅 · ( ( normCV𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑅 · 1 ) ) )
67 61 66 bitr4d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 𝐷 ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ≤ 𝑅 ↔ ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 ) )
68 breq2 ( 𝑘 = 𝐾 → ( ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝑘 ↔ ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ) )
69 68 ralbidv ( 𝑘 = 𝐾 → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝑘 ↔ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ) )
70 69 rabbidv ( 𝑘 = 𝐾 → { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝑘 } = { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } )
71 1 fvexi 𝑋 ∈ V
72 71 rabex { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } ∈ V
73 70 9 72 fvmpt ( 𝐾 ∈ ℕ → ( 𝐴𝐾 ) = { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } )
74 10 73 syl ( 𝜑 → ( 𝐴𝐾 ) = { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } )
75 74 eleq2d ( 𝜑 → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ↔ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } ) )
76 2fveq3 ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( 𝑁 ‘ ( 𝑡𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) )
77 76 breq1d ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ↔ ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
78 77 ralbidv ( 𝑧 = ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ↔ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
79 78 elrab ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } ↔ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
80 75 79 bitrdi ( 𝜑 → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ↔ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) ) )
81 80 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ ( 𝐴𝐾 ) ↔ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) ) )
82 38 67 81 3imtr3d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 → ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) ) )
83 rsp ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑡𝑇 → ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
84 83 com12 ( 𝑡𝑇 → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
85 84 ad2antlr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) )
86 xmet0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝑃 𝐷 𝑃 ) = 0 )
87 43 11 86 sylancr ( 𝜑 → ( 𝑃 𝐷 𝑃 ) = 0 )
88 12 rpge0d ( 𝜑 → 0 ≤ 𝑅 )
89 87 88 eqbrtrd ( 𝜑 → ( 𝑃 𝐷 𝑃 ) ≤ 𝑅 )
90 oveq2 ( 𝑧 = 𝑃 → ( 𝑃 𝐷 𝑧 ) = ( 𝑃 𝐷 𝑃 ) )
91 90 breq1d ( 𝑧 = 𝑃 → ( ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ↔ ( 𝑃 𝐷 𝑃 ) ≤ 𝑅 ) )
92 91 elrab ( 𝑃 ∈ { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ↔ ( 𝑃𝑋 ∧ ( 𝑃 𝐷 𝑃 ) ≤ 𝑅 ) )
93 11 89 92 sylanbrc ( 𝜑𝑃 ∈ { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } )
94 13 93 sseldd ( 𝜑𝑃 ∈ ( 𝐴𝐾 ) )
95 94 74 eleqtrd ( 𝜑𝑃 ∈ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } )
96 2fveq3 ( 𝑧 = 𝑃 → ( 𝑁 ‘ ( 𝑡𝑧 ) ) = ( 𝑁 ‘ ( 𝑡𝑃 ) ) )
97 96 breq1d ( 𝑧 = 𝑃 → ( ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ↔ ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) )
98 97 ralbidv ( 𝑧 = 𝑃 → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 ↔ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) )
99 98 elrab ( 𝑃 ∈ { 𝑧𝑋 ∣ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑧 ) ) ≤ 𝐾 } ↔ ( 𝑃𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) )
100 95 99 sylib ( 𝜑 → ( 𝑃𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) )
101 100 simprd ( 𝜑 → ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 )
102 101 r19.21bi ( ( 𝜑𝑡𝑇 ) → ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 )
103 102 adantr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 )
104 7 sselda ( ( 𝜑𝑡𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
105 eqid ( IndMet ‘ 𝑊 ) = ( IndMet ‘ 𝑊 )
106 eqid ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) = ( MetOpen ‘ ( IndMet ‘ 𝑊 ) )
107 eqid ( 𝑈 BLnOp 𝑊 ) = ( 𝑈 BLnOp 𝑊 )
108 3 105 4 106 107 26 6 blocn2 ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) )
109 4 mopntopon ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
110 43 109 ax-mp 𝐽 ∈ ( TopOn ‘ 𝑋 )
111 eqid ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
112 111 105 imsxmet ( 𝑊 ∈ NrmCVec → ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) )
113 106 mopntopon ( ( IndMet ‘ 𝑊 ) ∈ ( ∞Met ‘ ( BaseSet ‘ 𝑊 ) ) → ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) )
114 6 112 113 mp2b ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) )
115 iscncl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( BaseSet ‘ 𝑊 ) ) ) → ( 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( 𝑡𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) ) )
116 110 114 115 mp2an ( 𝑡 ∈ ( 𝐽 Cn ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( 𝑡𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
117 108 116 sylib ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( 𝑡𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
118 104 117 syl ( ( 𝜑𝑡𝑇 ) → ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ( Clsd ‘ ( MetOpen ‘ ( IndMet ‘ 𝑊 ) ) ) ( 𝑡𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
119 118 simpld ( ( 𝜑𝑡𝑇 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
120 119 adantr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
121 120 37 ffvelrnd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ∈ ( BaseSet ‘ 𝑊 ) )
122 111 2 nvcl ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ∈ ℝ )
123 6 121 122 sylancr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ∈ ℝ )
124 120 28 ffvelrnd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) )
125 111 2 nvcl ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡𝑃 ) ) ∈ ℝ )
126 6 124 125 sylancr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( 𝑡𝑃 ) ) ∈ ℝ )
127 10 nnred ( 𝜑𝐾 ∈ ℝ )
128 127 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝐾 ∈ ℝ )
129 le2add ( ( ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ∈ ℝ ∧ ( 𝑁 ‘ ( 𝑡𝑃 ) ) ∈ ℝ ) ∧ ( 𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) → ( ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ∧ ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
130 123 126 128 128 129 syl22anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ∧ ( 𝑁 ‘ ( 𝑡𝑃 ) ) ≤ 𝐾 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
131 103 130 mpan2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
132 52 fveq2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡 ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) = ( 𝑡 ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) )
133 6 a1i ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑊 ∈ NrmCVec )
134 eqid ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
135 134 107 bloln ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) ) → 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) )
136 26 6 135 mp3an12 ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) )
137 104 136 syl ( ( 𝜑𝑡𝑇 ) → 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) )
138 137 adantr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) )
139 eqid ( −𝑣𝑊 ) = ( −𝑣𝑊 )
140 1 47 139 134 lnosub ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋𝑃𝑋 ) ) → ( 𝑡 ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) = ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) )
141 27 133 138 37 28 140 syl32anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡 ‘ ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ( −𝑣𝑈 ) 𝑃 ) ) = ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) )
142 eqid ( ·𝑠OLD𝑊 ) = ( ·𝑠OLD𝑊 )
143 1 32 142 134 lnomul ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( 𝑅 ∈ ℂ ∧ 𝑥𝑋 ) ) → ( 𝑡 ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) = ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) )
144 27 133 138 30 31 143 syl32anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡 ‘ ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) = ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) )
145 132 141 144 3eqtr3d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) = ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) )
146 145 fveq2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) ) = ( 𝑁 ‘ ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) ) )
147 119 ffvelrnda ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑡𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
148 111 142 2 nvsge0 ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ∧ ( 𝑡𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) ) = ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) )
149 133 55 147 148 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( 𝑅 ( ·𝑠OLD𝑊 ) ( 𝑡𝑥 ) ) ) = ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) )
150 146 149 eqtrd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) ) = ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) )
151 111 139 2 nvmtri ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ∈ ( BaseSet ‘ 𝑊 ) ∧ ( 𝑡𝑃 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) )
152 133 121 124 151 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ( −𝑣𝑊 ) ( 𝑡𝑃 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) )
153 150 152 eqbrtrrd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) )
154 29 rpred ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → 𝑅 ∈ ℝ )
155 111 2 nvcl ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ∈ ℝ )
156 6 147 155 sylancr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ∈ ℝ )
157 154 156 remulcld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ∈ ℝ )
158 123 126 readdcld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ∈ ℝ )
159 15 rpred ( 𝜑 → ( 𝐾 + 𝐾 ) ∈ ℝ )
160 159 ad2antrr ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( 𝐾 + 𝐾 ) ∈ ℝ )
161 letr ( ( ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ∈ ℝ ∧ ( 𝐾 + 𝐾 ) ∈ ℝ ) → ( ( ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ∧ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
162 157 158 160 161 syl3anc ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ∧ ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
163 153 162 mpand ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) + ( 𝑁 ‘ ( 𝑡𝑃 ) ) ) ≤ ( 𝐾 + 𝐾 ) → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
164 131 163 syld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( 𝐾 + 𝐾 ) ) )
165 156 160 29 lemuldiv2d ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑅 · ( 𝑁 ‘ ( 𝑡𝑥 ) ) ) ≤ ( 𝐾 + 𝐾 ) ↔ ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
166 164 165 sylibd ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
167 85 166 syld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
168 167 adantld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ∈ 𝑋 ∧ ∀ 𝑡𝑇 ( 𝑁 ‘ ( 𝑡 ‘ ( 𝑃 ( +𝑣𝑈 ) ( 𝑅 ( ·𝑠OLD𝑈 ) 𝑥 ) ) ) ) ≤ 𝐾 ) → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
169 82 168 syld ( ( ( 𝜑𝑡𝑇 ) ∧ 𝑥𝑋 ) → ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
170 169 ralrimiva ( ( 𝜑𝑡𝑇 ) → ∀ 𝑥𝑋 ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) )
171 16 rpxrd ( 𝜑 → ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* )
172 171 adantr ( ( 𝜑𝑡𝑇 ) → ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* )
173 eqid ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
174 1 111 48 2 173 26 6 nmoubi ( ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ* ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ↔ ∀ 𝑥𝑋 ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) ) )
175 119 172 174 syl2anc ( ( 𝜑𝑡𝑇 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ↔ ∀ 𝑥𝑋 ( ( ( normCV𝑈 ) ‘ 𝑥 ) ≤ 1 → ( 𝑁 ‘ ( 𝑡𝑥 ) ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) ) )
176 170 175 mpbird ( ( 𝜑𝑡𝑇 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) )
177 176 ralrimiva ( 𝜑 → ∀ 𝑡𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) )
178 brralrspcev ( ( ( ( 𝐾 + 𝐾 ) / 𝑅 ) ∈ ℝ ∧ ∀ 𝑡𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ ( ( 𝐾 + 𝐾 ) / 𝑅 ) ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
179 17 177 178 syl2anc ( 𝜑 → ∃ 𝑑 ∈ ℝ ∀ 𝑡𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )