Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ubthlem2 Structured version   Visualization version   GIF version

Theorem ubthlem2 28057
 Description: Lemma for ubth 28059. Given that there is a closed ball 𝐵(𝑃, 𝑅) in 𝐴‘𝐾, for any 𝑥 ∈ 𝐵(0, 1), we have 𝑃 + 𝑅 · 𝑥 ∈ 𝐵(𝑃, 𝑅) and 𝑃 ∈ 𝐵(𝑃, 𝑅), so both of these have norm(𝑡(𝑧)) ≤ 𝐾 and so norm(𝑡(𝑥 )) ≤ (norm(𝑡(𝑃)) + norm(𝑡(𝑃 + 𝑅 · 𝑥))) / 𝑅 ≤ ( 𝐾 + 𝐾) / 𝑅, which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
ubthlem2 (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
Distinct variable groups:   𝑘,𝑐,𝑥,𝑧,𝐴   𝑡,𝑐,𝐷,𝑘,𝑥,𝑧   𝑘,𝐽,𝑡,𝑥   𝑘,𝑑,𝑡,𝑥,𝑧,𝐾   𝑐,𝑑,𝑁,𝑘,𝑡,𝑥,𝑧   𝑡,𝑃,𝑧   𝜑,𝑐,𝑘,𝑡,𝑥   𝑅,𝑑,𝑡,𝑥,𝑧   𝑇,𝑐,𝑑,𝑘,𝑡,𝑥,𝑧   𝑈,𝑐,𝑑,𝑡,𝑥,𝑧   𝑊,𝑐,𝑑,𝑡,𝑥   𝑋,𝑐,𝑑,𝑘,𝑡,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑑)   𝐴(𝑡,𝑑)   𝐷(𝑑)   𝑃(𝑥,𝑘,𝑐,𝑑)   𝑅(𝑘,𝑐)   𝑈(𝑘)   𝐽(𝑧,𝑐,𝑑)   𝐾(𝑐)   𝑊(𝑧,𝑘)

Proof of Theorem ubthlem2
StepHypRef Expression
1 ubthlem.10 . . . . . 6 (𝜑𝐾 ∈ ℕ)
21nnrpd 12083 . . . . 5 (𝜑𝐾 ∈ ℝ+)
32, 2rpaddcld 12100 . . . 4 (𝜑 → (𝐾 + 𝐾) ∈ ℝ+)
4 ubthlem.12 . . . 4 (𝜑𝑅 ∈ ℝ+)
53, 4rpdivcld 12102 . . 3 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ+)
65rpred 12085 . 2 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ)
7 oveq2 6822 . . . . . . . . . 10 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑃𝐷𝑧) = (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))))
87breq1d 4814 . . . . . . . . 9 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅))
9 eleq1 2827 . . . . . . . . 9 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑧 ∈ (𝐴𝐾) ↔ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾)))
108, 9imbi12d 333 . . . . . . . 8 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)) ↔ ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾))))
11 ubthlem.13 . . . . . . . . . 10 (𝜑 → {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴𝐾))
12 rabss 3820 . . . . . . . . . 10 ({𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴𝐾) ↔ ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
1311, 12sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
1413ad2antrr 764 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
15 ubthlem.5 . . . . . . . . . . 11 𝑈 ∈ CBan
16 bnnv 28052 . . . . . . . . . . 11 (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
1715, 16ax-mp 5 . . . . . . . . . 10 𝑈 ∈ NrmCVec
1817a1i 11 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑈 ∈ NrmCVec)
19 ubthlem.11 . . . . . . . . . 10 (𝜑𝑃𝑋)
2019ad2antrr 764 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑃𝑋)
214ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ+)
2221rpcnd 12087 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℂ)
23 simpr 479 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑥𝑋)
24 ubth.1 . . . . . . . . . . 11 𝑋 = (BaseSet‘𝑈)
25 eqid 2760 . . . . . . . . . . 11 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
2624, 25nvscl 27811 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝑅 ∈ ℂ ∧ 𝑥𝑋) → (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋)
2718, 22, 23, 26syl3anc 1477 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋)
28 eqid 2760 . . . . . . . . . 10 ( +𝑣𝑈) = ( +𝑣𝑈)
2924, 28nvgcl 27805 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋) → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋)
3018, 20, 27, 29syl3anc 1477 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋)
3110, 14, 30rspcdva 3455 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾)))
32 ubthlem.3 . . . . . . . . . . . . . . . 16 𝐷 = (IndMet‘𝑈)
3324, 32cbncms 28051 . . . . . . . . . . . . . . 15 (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
3415, 33ax-mp 5 . . . . . . . . . . . . . 14 𝐷 ∈ (CMet‘𝑋)
35 cmetmet 23304 . . . . . . . . . . . . . 14 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
36 metxmet 22360 . . . . . . . . . . . . . 14 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
3734, 35, 36mp2b 10 . . . . . . . . . . . . 13 𝐷 ∈ (∞Met‘𝑋)
3837a1i 11 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝐷 ∈ (∞Met‘𝑋))
39 xmetsym 22373 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋 ∧ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃))
4038, 20, 30, 39syl3anc 1477 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃))
41 eqid 2760 . . . . . . . . . . . . 13 ( −𝑣𝑈) = ( −𝑣𝑈)
42 eqid 2760 . . . . . . . . . . . . 13 (normCV𝑈) = (normCV𝑈)
4324, 41, 42, 32imsdval 27871 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋𝑃𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)))
4418, 30, 20, 43syl3anc 1477 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)))
4524, 28, 41nvpncan2 27838 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃) = (𝑅( ·𝑠OLD𝑈)𝑥))
4618, 20, 27, 45syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃) = (𝑅( ·𝑠OLD𝑈)𝑥))
4746fveq2d 6357 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)))
4840, 44, 473eqtrd 2798 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)))
4921rprege0d 12092 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
5024, 25, 42nvsge0 27849 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑥𝑋) → ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅 · ((normCV𝑈)‘𝑥)))
5118, 49, 23, 50syl3anc 1477 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅 · ((normCV𝑈)‘𝑥)))
5248, 51eqtrd 2794 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = (𝑅 · ((normCV𝑈)‘𝑥)))
5322mulid1d 10269 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · 1) = 𝑅)
5453eqcomd 2766 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 = (𝑅 · 1))
5552, 54breq12d 4817 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 ↔ (𝑅 · ((normCV𝑈)‘𝑥)) ≤ (𝑅 · 1)))
5624, 42nvcl 27846 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑥𝑋) → ((normCV𝑈)‘𝑥) ∈ ℝ)
5717, 56mpan 708 . . . . . . . . . 10 (𝑥𝑋 → ((normCV𝑈)‘𝑥) ∈ ℝ)
5857adantl 473 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘𝑥) ∈ ℝ)
59 1red 10267 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 1 ∈ ℝ)
6058, 59, 21lemul2d 12129 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 ↔ (𝑅 · ((normCV𝑈)‘𝑥)) ≤ (𝑅 · 1)))
6155, 60bitr4d 271 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 ↔ ((normCV𝑈)‘𝑥) ≤ 1))
62 breq2 4808 . . . . . . . . . . . . . 14 (𝑘 = 𝐾 → ((𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡𝑧)) ≤ 𝐾))
6362ralbidv 3124 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾))
6463rabbidv 3329 . . . . . . . . . . . 12 (𝑘 = 𝐾 → {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
65 ubthlem.9 . . . . . . . . . . . 12 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
66 fvex 6363 . . . . . . . . . . . . . 14 (BaseSet‘𝑈) ∈ V
6724, 66eqeltri 2835 . . . . . . . . . . . . 13 𝑋 ∈ V
6867rabex 4964 . . . . . . . . . . . 12 {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ∈ V
6964, 65, 68fvmpt 6445 . . . . . . . . . . 11 (𝐾 ∈ ℕ → (𝐴𝐾) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
701, 69syl 17 . . . . . . . . . 10 (𝜑 → (𝐴𝐾) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
7170eleq2d 2825 . . . . . . . . 9 (𝜑 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾}))
72 fveq2 6353 . . . . . . . . . . . . 13 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑡𝑧) = (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))))
7372fveq2d 6357 . . . . . . . . . . . 12 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑁‘(𝑡𝑧)) = (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))))
7473breq1d 4814 . . . . . . . . . . 11 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → ((𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7574ralbidv 3124 . . . . . . . . . 10 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7675elrab 3504 . . . . . . . . 9 ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7771, 76syl6bb 276 . . . . . . . 8 (𝜑 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
7877ad2antrr 764 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
7931, 61, 783imtr3d 282 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
80 rsp 3067 . . . . . . . . . 10 (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑡𝑇 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
8180com12 32 . . . . . . . . 9 (𝑡𝑇 → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
8281ad2antlr 765 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
83 xmet0 22368 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋) → (𝑃𝐷𝑃) = 0)
8437, 19, 83sylancr 698 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃𝐷𝑃) = 0)
854rpge0d 12089 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑅)
8684, 85eqbrtrd 4826 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃𝐷𝑃) ≤ 𝑅)
87 oveq2 6822 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑃 → (𝑃𝐷𝑧) = (𝑃𝐷𝑃))
8887breq1d 4814 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑃 → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷𝑃) ≤ 𝑅))
8988elrab 3504 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ↔ (𝑃𝑋 ∧ (𝑃𝐷𝑃) ≤ 𝑅))
9019, 86, 89sylanbrc 701 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅})
9111, 90sseldd 3745 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (𝐴𝐾))
9291, 70eleqtrd 2841 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
93 fveq2 6353 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑃 → (𝑡𝑧) = (𝑡𝑃))
9493fveq2d 6357 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑃 → (𝑁‘(𝑡𝑧)) = (𝑁‘(𝑡𝑃)))
9594breq1d 4814 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑃 → ((𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9695ralbidv 3124 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑃 → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9796elrab 3504 . . . . . . . . . . . . . . 15 (𝑃 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ↔ (𝑃𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9892, 97sylib 208 . . . . . . . . . . . . . 14 (𝜑 → (𝑃𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9998simprd 482 . . . . . . . . . . . . 13 (𝜑 → ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾)
10099r19.21bi 3070 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝑁‘(𝑡𝑃)) ≤ 𝐾)
101100adantr 472 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑃)) ≤ 𝐾)
102 ubthlem.6 . . . . . . . . . . . . 13 𝑊 ∈ NrmCVec
103 ubthlem.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ (𝑈 BLnOp 𝑊))
104103sselda 3744 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊))
105 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (IndMet‘𝑊) = (IndMet‘𝑊)
106 ubthlem.4 . . . . . . . . . . . . . . . . . . 19 𝐽 = (MetOpen‘𝐷)
107 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
108 eqid 2760 . . . . . . . . . . . . . . . . . . 19 (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
10932, 105, 106, 107, 108, 17, 102blocn2 27993 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
110106mopntopon 22465 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
11137, 110ax-mp 5 . . . . . . . . . . . . . . . . . . 19 𝐽 ∈ (TopOn‘𝑋)
112 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (BaseSet‘𝑊) = (BaseSet‘𝑊)
113112, 105imsxmet 27877 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
114107mopntopon 22465 . . . . . . . . . . . . . . . . . . . 20 ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
115102, 113, 114mp2b 10 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
116 iscncl 21295 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽))))
117111, 115, 116mp2an 710 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
118109, 117sylib 208 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
119104, 118syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
120119simpld 477 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
121120adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑡:𝑋⟶(BaseSet‘𝑊))
122121, 30ffvelrnd 6524 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊))
123 ubth.2 . . . . . . . . . . . . . 14 𝑁 = (normCV𝑊)
124112, 123nvcl 27846 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ)
125102, 122, 124sylancr 698 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ)
126121, 20ffvelrnd 6524 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑃) ∈ (BaseSet‘𝑊))
127112, 123nvcl 27846 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡𝑃)) ∈ ℝ)
128102, 126, 127sylancr 698 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑃)) ∈ ℝ)
1291nnred 11247 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ)
130129ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝐾 ∈ ℝ)
131 le2add 10722 . . . . . . . . . . . 12 ((((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ ∧ (𝑁‘(𝑡𝑃)) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ)) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
132125, 128, 130, 130, 131syl22anc 1478 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
133101, 132mpan2d 712 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
13446fveq2d 6357 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)))
135102a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑊 ∈ NrmCVec)
136 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 (𝑈 LnOp 𝑊) = (𝑈 LnOp 𝑊)
137136, 108bloln 27969 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 BLnOp 𝑊)) → 𝑡 ∈ (𝑈 LnOp 𝑊))
13817, 102, 137mp3an12 1563 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝑈 LnOp 𝑊))
139104, 138syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝑈 LnOp 𝑊))
140139adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑡 ∈ (𝑈 LnOp 𝑊))
141 eqid 2760 . . . . . . . . . . . . . . . . 17 ( −𝑣𝑊) = ( −𝑣𝑊)
14224, 41, 141, 136lnosub 27944 . . . . . . . . . . . . . . . 16 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋𝑃𝑋)) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)))
14318, 135, 140, 30, 20, 142syl32anc 1485 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)))
144 eqid 2760 . . . . . . . . . . . . . . . . 17 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
14524, 25, 144, 136lnomul 27945 . . . . . . . . . . . . . . . 16 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ (𝑅 ∈ ℂ ∧ 𝑥𝑋)) → (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
14618, 135, 140, 22, 23, 145syl32anc 1485 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
147134, 143, 1463eqtr3d 2802 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
148147fveq2d 6357 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) = (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))))
149120ffvelrnda 6523 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑥) ∈ (BaseSet‘𝑊))
150112, 144, 123nvsge0 27849 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ (𝑡𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))) = (𝑅 · (𝑁‘(𝑡𝑥))))
151135, 49, 149, 150syl3anc 1477 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))) = (𝑅 · (𝑁‘(𝑡𝑥))))
152148, 151eqtrd 2794 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) = (𝑅 · (𝑁‘(𝑡𝑥))))
153112, 141, 123nvmtri 27856 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊) ∧ (𝑡𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
154135, 122, 126, 153syl3anc 1477 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
155152, 154eqbrtrrd 4828 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
15621rpred 12085 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ)
157112, 123nvcl 27846 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ (𝑡𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
158102, 149, 157sylancr 698 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
159156, 158remulcld 10282 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · (𝑁‘(𝑡𝑥))) ∈ ℝ)
160125, 128readdcld 10281 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∈ ℝ)
1613rpred 12085 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 𝐾) ∈ ℝ)
162161ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝐾 + 𝐾) ∈ ℝ)
163 letr 10343 . . . . . . . . . . . 12 (((𝑅 · (𝑁‘(𝑡𝑥))) ∈ ℝ ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∈ ℝ ∧ (𝐾 + 𝐾) ∈ ℝ) → (((𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
164159, 160, 162, 163syl3anc 1477 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
165155, 164mpand 713 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
166133, 165syld 47 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
167158, 162, 21lemuldiv2d 12135 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾) ↔ (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
168166, 167sylibd 229 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
16982, 168syld 47 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
170169adantld 484 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾) → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
17179, 170syld 47 . . . . 5 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
172171ralrimiva 3104 . . . 4 ((𝜑𝑡𝑇) → ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
1735rpxrd 12086 . . . . . 6 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*)
174173adantr 472 . . . . 5 ((𝜑𝑡𝑇) → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*)
175 eqid 2760 . . . . . 6 (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊)
17624, 112, 42, 123, 175, 17, 102nmoubi 27957 . . . . 5 ((𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))))
177120, 174, 176syl2anc 696 . . . 4 ((𝜑𝑡𝑇) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))))
178172, 177mpbird 247 . . 3 ((𝜑𝑡𝑇) → ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))
179178ralrimiva 3104 . 2 (𝜑 → ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))
180 breq2 4808 . . . 4 (𝑑 = ((𝐾 + 𝐾) / 𝑅) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)))
181180ralbidv 3124 . . 3 (𝑑 = ((𝐾 + 𝐾) / 𝑅) → (∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)))
182181rspcev 3449 . 2 ((((𝐾 + 𝐾) / 𝑅) ∈ ℝ ∧ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) → ∃𝑑 ∈ ℝ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
1836, 179, 182syl2anc 696 1 (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  ∀wral 3050  ∃wrex 3051  {crab 3054  Vcvv 3340   ⊆ wss 3715   class class class wbr 4804   ↦ cmpt 4881  ◡ccnv 5265   “ cima 5269  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814  ℂcc 10146  ℝcr 10147  0cc0 10148  1c1 10149   + caddc 10151   · cmul 10153  ℝ*cxr 10285   ≤ cle 10287   / cdiv 10896  ℕcn 11232  ℝ+crp 12045  ∞Metcxmt 19953  Metcme 19954  MetOpencmopn 19958  TopOnctopon 20937  Clsdccld 21042   Cn ccn 21250  CMetcms 23272  NrmCVeccnv 27769   +𝑣 cpv 27770  BaseSetcba 27771   ·𝑠OLD cns 27772   −𝑣 cnsb 27774  normCVcnmcv 27775  IndMetcims 27776   LnOp clno 27925   normOpOLD cnmoo 27926   BLnOp cblo 27927  CBanccbn 28048 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-n0 11505  df-z 11590  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-topgen 16326  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-top 20921  df-topon 20938  df-bases 20972  df-cld 21045  df-cn 21253  df-cnp 21254  df-cmet 23275  df-grpo 27677  df-gid 27678  df-ginv 27679  df-gdiv 27680  df-ablo 27729  df-vc 27744  df-nv 27777  df-va 27780  df-ba 27781  df-sm 27782  df-0v 27783  df-vs 27784  df-nmcv 27785  df-ims 27786  df-lno 27929  df-nmoo 27930  df-blo 27931  df-0o 27932  df-cbn 28049 This theorem is referenced by:  ubthlem3  28058
 Copyright terms: Public domain W3C validator