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

Theorem ubthlem2 28658
 Description: Lemma for ubth 28660. 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 12421 . . . . 5 (𝜑𝐾 ∈ ℝ+)
32, 2rpaddcld 12438 . . . 4 (𝜑 → (𝐾 + 𝐾) ∈ ℝ+)
4 ubthlem.12 . . . 4 (𝜑𝑅 ∈ ℝ+)
53, 4rpdivcld 12440 . . 3 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ+)
65rpred 12423 . 2 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ)
7 oveq2 7147 . . . . . . . . . 10 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑃𝐷𝑧) = (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))))
87breq1d 5043 . . . . . . . . 9 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅))
9 eleq1 2880 . . . . . . . . 9 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑧 ∈ (𝐴𝐾) ↔ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾)))
108, 9imbi12d 348 . . . . . . . 8 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)) ↔ ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾))))
11 ubthlem.13 . . . . . . . . . 10 (𝜑 → {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴𝐾))
12 rabss 4002 . . . . . . . . . 10 ({𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴𝐾) ↔ ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
1311, 12sylib 221 . . . . . . . . 9 (𝜑 → ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
1413ad2antrr 725 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ∀𝑧𝑋 ((𝑃𝐷𝑧) ≤ 𝑅𝑧 ∈ (𝐴𝐾)))
15 ubthlem.5 . . . . . . . . . . 11 𝑈 ∈ CBan
16 bnnv 28653 . . . . . . . . . . 11 (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
1715, 16ax-mp 5 . . . . . . . . . 10 𝑈 ∈ NrmCVec
1817a1i 11 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑈 ∈ NrmCVec)
19 ubthlem.11 . . . . . . . . . 10 (𝜑𝑃𝑋)
2019ad2antrr 725 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑃𝑋)
214ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ+)
2221rpcnd 12425 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℂ)
23 simpr 488 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑥𝑋)
24 ubth.1 . . . . . . . . . . 11 𝑋 = (BaseSet‘𝑈)
25 eqid 2801 . . . . . . . . . . 11 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
2624, 25nvscl 28413 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝑅 ∈ ℂ ∧ 𝑥𝑋) → (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋)
2718, 22, 23, 26syl3anc 1368 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋)
28 eqid 2801 . . . . . . . . . 10 ( +𝑣𝑈) = ( +𝑣𝑈)
2924, 28nvgcl 28407 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋) → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋)
3018, 20, 27, 29syl3anc 1368 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋)
3110, 14, 30rspcdva 3576 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾)))
32 ubthlem.3 . . . . . . . . . . . . . . . 16 𝐷 = (IndMet‘𝑈)
3324, 32cbncms 28652 . . . . . . . . . . . . . . 15 (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
3415, 33ax-mp 5 . . . . . . . . . . . . . 14 𝐷 ∈ (CMet‘𝑋)
35 cmetmet 23894 . . . . . . . . . . . . . 14 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
36 metxmet 22945 . . . . . . . . . . . . . 14 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
3734, 35, 36mp2b 10 . . . . . . . . . . . . 13 𝐷 ∈ (∞Met‘𝑋)
3837a1i 11 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝐷 ∈ (∞Met‘𝑋))
39 xmetsym 22958 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋 ∧ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃))
4038, 20, 30, 39syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃))
41 eqid 2801 . . . . . . . . . . . . 13 ( −𝑣𝑈) = ( −𝑣𝑈)
42 eqid 2801 . . . . . . . . . . . . 13 (normCV𝑈) = (normCV𝑈)
4324, 41, 42, 32imsdval 28473 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋𝑃𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)))
4418, 30, 20, 43syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))𝐷𝑃) = ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)))
4524, 28, 41nvpncan2 28440 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ 𝑃𝑋 ∧ (𝑅( ·𝑠OLD𝑈)𝑥) ∈ 𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃) = (𝑅( ·𝑠OLD𝑈)𝑥))
4618, 20, 27, 45syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃) = (𝑅( ·𝑠OLD𝑈)𝑥))
4746fveq2d 6653 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)))
4840, 44, 473eqtrd 2840 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)))
4921rprege0d 12430 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
5024, 25, 42nvsge0 28451 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ 𝑥𝑋) → ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅 · ((normCV𝑈)‘𝑥)))
5118, 49, 23, 50syl3anc 1368 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅 · ((normCV𝑈)‘𝑥)))
5248, 51eqtrd 2836 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) = (𝑅 · ((normCV𝑈)‘𝑥)))
5322mulid1d 10651 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · 1) = 𝑅)
5453eqcomd 2807 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 = (𝑅 · 1))
5552, 54breq12d 5046 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 ↔ (𝑅 · ((normCV𝑈)‘𝑥)) ≤ (𝑅 · 1)))
5624, 42nvcl 28448 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑥𝑋) → ((normCV𝑈)‘𝑥) ∈ ℝ)
5717, 56mpan 689 . . . . . . . . . 10 (𝑥𝑋 → ((normCV𝑈)‘𝑥) ∈ ℝ)
5857adantl 485 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((normCV𝑈)‘𝑥) ∈ ℝ)
59 1red 10635 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 1 ∈ ℝ)
6058, 59, 21lemul2d 12467 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 ↔ (𝑅 · ((normCV𝑈)‘𝑥)) ≤ (𝑅 · 1)))
6155, 60bitr4d 285 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃𝐷(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ≤ 𝑅 ↔ ((normCV𝑈)‘𝑥) ≤ 1))
62 breq2 5037 . . . . . . . . . . . . . 14 (𝑘 = 𝐾 → ((𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡𝑧)) ≤ 𝐾))
6362ralbidv 3165 . . . . . . . . . . . . 13 (𝑘 = 𝐾 → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾))
6463rabbidv 3430 . . . . . . . . . . . 12 (𝑘 = 𝐾 → {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
65 ubthlem.9 . . . . . . . . . . . 12 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
6624fvexi 6663 . . . . . . . . . . . . 13 𝑋 ∈ V
6766rabex 5202 . . . . . . . . . . . 12 {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ∈ V
6864, 65, 67fvmpt 6749 . . . . . . . . . . 11 (𝐾 ∈ ℕ → (𝐴𝐾) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
691, 68syl 17 . . . . . . . . . 10 (𝜑 → (𝐴𝐾) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
7069eleq2d 2878 . . . . . . . . 9 (𝜑 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾}))
71 2fveq3 6654 . . . . . . . . . . . 12 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (𝑁‘(𝑡𝑧)) = (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))))
7271breq1d 5043 . . . . . . . . . . 11 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → ((𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7372ralbidv 3165 . . . . . . . . . 10 (𝑧 = (𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7473elrab 3631 . . . . . . . . 9 ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7570, 74syl6bb 290 . . . . . . . 8 (𝜑 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
7675ad2antrr 725 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ (𝐴𝐾) ↔ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
7731, 61, 763imtr3d 296 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 → ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾)))
78 rsp 3173 . . . . . . . . . 10 (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑡𝑇 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
7978com12 32 . . . . . . . . 9 (𝑡𝑇 → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
8079ad2antlr 726 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾))
81 xmet0 22953 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃𝑋) → (𝑃𝐷𝑃) = 0)
8237, 19, 81sylancr 590 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃𝐷𝑃) = 0)
834rpge0d 12427 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 𝑅)
8482, 83eqbrtrd 5055 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃𝐷𝑃) ≤ 𝑅)
85 oveq2 7147 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑃 → (𝑃𝐷𝑧) = (𝑃𝐷𝑃))
8685breq1d 5043 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑃 → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷𝑃) ≤ 𝑅))
8786elrab 3631 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ↔ (𝑃𝑋 ∧ (𝑃𝐷𝑃) ≤ 𝑅))
8819, 84, 87sylanbrc 586 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ {𝑧𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅})
8911, 88sseldd 3919 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (𝐴𝐾))
9089, 69eleqtrd 2895 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾})
91 2fveq3 6654 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑃 → (𝑁‘(𝑡𝑧)) = (𝑁‘(𝑡𝑃)))
9291breq1d 5043 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑃 → ((𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9392ralbidv 3165 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑃 → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾 ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9493elrab 3631 . . . . . . . . . . . . . . 15 (𝑃 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝐾} ↔ (𝑃𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9590, 94sylib 221 . . . . . . . . . . . . . 14 (𝜑 → (𝑃𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾))
9695simprd 499 . . . . . . . . . . . . 13 (𝜑 → ∀𝑡𝑇 (𝑁‘(𝑡𝑃)) ≤ 𝐾)
9796r19.21bi 3176 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → (𝑁‘(𝑡𝑃)) ≤ 𝐾)
9897adantr 484 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑃)) ≤ 𝐾)
99 ubthlem.6 . . . . . . . . . . . . 13 𝑊 ∈ NrmCVec
100 ubthlem.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇 ⊆ (𝑈 BLnOp 𝑊))
101100sselda 3918 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊))
102 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (IndMet‘𝑊) = (IndMet‘𝑊)
103 ubthlem.4 . . . . . . . . . . . . . . . . . . 19 𝐽 = (MetOpen‘𝐷)
104 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊))
105 eqid 2801 . . . . . . . . . . . . . . . . . . 19 (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
10632, 102, 103, 104, 105, 17, 99blocn2 28595 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
107103mopntopon 23050 . . . . . . . . . . . . . . . . . . . 20 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
10837, 107ax-mp 5 . . . . . . . . . . . . . . . . . . 19 𝐽 ∈ (TopOn‘𝑋)
109 eqid 2801 . . . . . . . . . . . . . . . . . . . . 21 (BaseSet‘𝑊) = (BaseSet‘𝑊)
110109, 102imsxmet 28479 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
111104mopntopon 23050 . . . . . . . . . . . . . . . . . . . 20 ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
11299, 110, 111mp2b 10 . . . . . . . . . . . . . . . . . . 19 (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
113 iscncl 21878 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽))))
114108, 112, 113mp2an 691 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
115106, 114sylib 221 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
116101, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
117116simpld 498 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
118117adantr 484 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑡:𝑋⟶(BaseSet‘𝑊))
119118, 30ffvelrnd 6833 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊))
120 ubth.2 . . . . . . . . . . . . . 14 𝑁 = (normCV𝑊)
121109, 120nvcl 28448 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ)
12299, 119, 121sylancr 590 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ)
123118, 20ffvelrnd 6833 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑃) ∈ (BaseSet‘𝑊))
124109, 120nvcl 28448 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡𝑃)) ∈ ℝ)
12599, 123, 124sylancr 590 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑃)) ∈ ℝ)
1261nnred 11644 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ)
127126ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝐾 ∈ ℝ)
128 le2add 11115 . . . . . . . . . . . 12 ((((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ∈ ℝ ∧ (𝑁‘(𝑡𝑃)) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ)) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
129122, 125, 127, 127, 128syl22anc 837 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
13098, 129mpan2d 693 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)))
13146fveq2d 6653 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)))
13299a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑊 ∈ NrmCVec)
133 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 (𝑈 LnOp 𝑊) = (𝑈 LnOp 𝑊)
134133, 105bloln 28571 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 BLnOp 𝑊)) → 𝑡 ∈ (𝑈 LnOp 𝑊))
13517, 99, 134mp3an12 1448 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝑈 LnOp 𝑊))
136101, 135syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝑈 LnOp 𝑊))
137136adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑡 ∈ (𝑈 LnOp 𝑊))
138 eqid 2801 . . . . . . . . . . . . . . . . 17 ( −𝑣𝑊) = ( −𝑣𝑊)
13924, 41, 138, 133lnosub 28546 . . . . . . . . . . . . . . . 16 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ ((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋𝑃𝑋)) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)))
14018, 132, 137, 30, 20, 139syl32anc 1375 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))( −𝑣𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)))
141 eqid 2801 . . . . . . . . . . . . . . . . 17 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
14224, 25, 141, 133lnomul 28547 . . . . . . . . . . . . . . . 16 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ (𝑅 ∈ ℂ ∧ 𝑥𝑋)) → (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
14318, 132, 137, 22, 23, 142syl32anc 1375 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡‘(𝑅( ·𝑠OLD𝑈)𝑥)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
144131, 140, 1433eqtr3d 2844 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃)) = (𝑅( ·𝑠OLD𝑊)(𝑡𝑥)))
145144fveq2d 6653 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) = (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))))
146117ffvelrnda 6832 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑥) ∈ (BaseSet‘𝑊))
147109, 141, 120nvsge0 28451 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) ∧ (𝑡𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))) = (𝑅 · (𝑁‘(𝑡𝑥))))
148132, 49, 146, 147syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑅( ·𝑠OLD𝑊)(𝑡𝑥))) = (𝑅 · (𝑁‘(𝑡𝑥))))
149145, 148eqtrd 2836 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) = (𝑅 · (𝑁‘(𝑡𝑥))))
150109, 138, 120nvmtri 28458 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥))) ∈ (BaseSet‘𝑊) ∧ (𝑡𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
151132, 119, 123, 150syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))( −𝑣𝑊)(𝑡𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
152149, 151eqbrtrrd 5057 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))))
15321rpred 12423 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ)
154109, 120nvcl 28448 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ (𝑡𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
15599, 146, 154sylancr 590 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
156153, 155remulcld 10664 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑅 · (𝑁‘(𝑡𝑥))) ∈ ℝ)
157122, 125readdcld 10663 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∈ ℝ)
1583rpred 12423 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 𝐾) ∈ ℝ)
159158ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝐾 + 𝐾) ∈ ℝ)
160 letr 10727 . . . . . . . . . . . 12 (((𝑅 · (𝑁‘(𝑡𝑥))) ∈ ℝ ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∈ ℝ ∧ (𝐾 + 𝐾) ∈ ℝ) → (((𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
161156, 157, 159, 160syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑅 · (𝑁‘(𝑡𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
162152, 161mpand 694 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) + (𝑁‘(𝑡𝑃))) ≤ (𝐾 + 𝐾) → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
163130, 162syld 47 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾)))
164155, 159, 21lemuldiv2d 12473 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑅 · (𝑁‘(𝑡𝑥))) ≤ (𝐾 + 𝐾) ↔ (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
165163, 164sylibd 242 . . . . . . . 8 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
16680, 165syld 47 . . . . . . 7 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
167166adantld 494 . . . . . 6 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣𝑈)(𝑅( ·𝑠OLD𝑈)𝑥)))) ≤ 𝐾) → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
16877, 167syld 47 . . . . 5 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
169168ralrimiva 3152 . . . 4 ((𝜑𝑡𝑇) → ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))
1705rpxrd 12424 . . . . . 6 (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*)
171170adantr 484 . . . . 5 ((𝜑𝑡𝑇) → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*)
172 eqid 2801 . . . . . 6 (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊)
17324, 109, 42, 120, 172, 17, 99nmoubi 28559 . . . . 5 ((𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))))
174117, 171, 173syl2anc 587 . . . 4 ((𝜑𝑡𝑇) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥𝑋 (((normCV𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))))
175169, 174mpbird 260 . . 3 ((𝜑𝑡𝑇) → ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))
176175ralrimiva 3152 . 2 (𝜑 → ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))
177 brralrspcev 5093 . 2 ((((𝐾 + 𝐾) / 𝑅) ∈ ℝ ∧ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) → ∃𝑑 ∈ ℝ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
1786, 176, 177syl2anc 587 1 (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ∃wrex 3110  {crab 3113   ⊆ wss 3884   class class class wbr 5033   ↦ cmpt 5113  ◡ccnv 5522   “ cima 5526  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  ℝ*cxr 10667   ≤ cle 10669   / cdiv 11290  ℕcn 11629  ℝ+crp 12381  ∞Metcxmet 20080  Metcmet 20081  MetOpencmopn 20085  TopOnctopon 21519  Clsdccld 21625   Cn ccn 21833  CMetccmet 23862  NrmCVeccnv 28371   +𝑣 cpv 28372  BaseSetcba 28373   ·𝑠OLD cns 28374   −𝑣 cnsb 28376  normCVcnmcv 28377  IndMetcims 28378   LnOp clno 28527   normOpOLD cnmoo 28528   BLnOp cblo 28529  CBanccbn 28649 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-inf 8895  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-seq 13369  df-exp 13430  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-topgen 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21503  df-topon 21520  df-bases 21555  df-cld 21628  df-cn 21836  df-cnp 21837  df-cmet 23865  df-grpo 28280  df-gid 28281  df-ginv 28282  df-gdiv 28283  df-ablo 28332  df-vc 28346  df-nv 28379  df-va 28382  df-ba 28383  df-sm 28384  df-0v 28385  df-vs 28386  df-nmcv 28387  df-ims 28388  df-lno 28531  df-nmoo 28532  df-blo 28533  df-0o 28534  df-cbn 28650 This theorem is referenced by:  ubthlem3  28659
 Copyright terms: Public domain W3C validator