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 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )