Proof of Theorem ubthlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ubthlem.10 | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 2 | 1 | nnrpd 13075 | . . . . 5
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 3 | 2, 2 | rpaddcld 13092 | . . . 4
⊢ (𝜑 → (𝐾 + 𝐾) ∈
ℝ+) | 
| 4 |  | ubthlem.12 | . . . 4
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 5 | 3, 4 | rpdivcld 13094 | . . 3
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ+) | 
| 6 | 5 | rpred 13077 | . 2
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ) | 
| 7 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑃𝐷𝑧) = (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) | 
| 8 | 7 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅)) | 
| 9 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑧 ∈ (𝐴‘𝐾) ↔ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾))) | 
| 10 | 8, 9 | imbi12d 344 | . . . . . . . 8
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾)) ↔ ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾)))) | 
| 11 |  | ubthlem.13 | . . . . . . . . . 10
⊢ (𝜑 → {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾)) | 
| 12 |  | rabss 4072 | . . . . . . . . . 10
⊢ ({𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾) ↔ ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) | 
| 13 | 11, 12 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) | 
| 14 | 13 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) | 
| 15 |  | ubthlem.5 | . . . . . . . . . . 11
⊢ 𝑈 ∈ CBan | 
| 16 |  | bnnv 30885 | . . . . . . . . . . 11
⊢ (𝑈 ∈ CBan → 𝑈 ∈
NrmCVec) | 
| 17 | 15, 16 | ax-mp 5 | . . . . . . . . . 10
⊢ 𝑈 ∈ NrmCVec | 
| 18 | 17 | a1i 11 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑈 ∈ NrmCVec) | 
| 19 |  | ubthlem.11 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ 𝑋) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ 𝑋) | 
| 21 | 4 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ+) | 
| 22 | 21 | rpcnd 13079 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈ ℂ) | 
| 23 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 24 |  | ubth.1 | . . . . . . . . . . 11
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 25 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) | 
| 26 | 24, 25 | nvscl 30645 | . . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑅 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) | 
| 27 | 18, 22, 23, 26 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) | 
| 28 |  | eqid 2737 | . . . . . . . . . 10
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) | 
| 29 | 24, 28 | nvgcl 30639 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) | 
| 30 | 18, 20, 27, 29 | syl3anc 1373 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) | 
| 31 | 10, 14, 30 | rspcdva 3623 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾))) | 
| 32 |  | ubthlem.3 | . . . . . . . . . . . . . . . 16
⊢ 𝐷 = (IndMet‘𝑈) | 
| 33 | 24, 32 | cbncms 30884 | . . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) | 
| 34 | 15, 33 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ 𝐷 ∈ (CMet‘𝑋) | 
| 35 |  | cmetmet 25320 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | 
| 36 |  | metxmet 24344 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 37 | 34, 35, 36 | mp2b 10 | . . . . . . . . . . . . 13
⊢ 𝐷 ∈ (∞Met‘𝑋) | 
| 38 | 37 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) | 
| 39 |  | xmetsym 24357 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃)) | 
| 40 | 38, 20, 30, 39 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃)) | 
| 41 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) | 
| 42 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(normCV‘𝑈) = (normCV‘𝑈) | 
| 43 | 24, 41, 42, 32 | imsdval 30705 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑃( +𝑣
‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃))) | 
| 44 | 18, 30, 20, 43 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃))) | 
| 45 | 24, 28, 41 | nvpncan2 30672 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃) = (𝑅( ·𝑠OLD
‘𝑈)𝑥)) | 
| 46 | 18, 20, 27, 45 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃) = (𝑅( ·𝑠OLD
‘𝑈)𝑥)) | 
| 47 | 46 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) | 
| 48 | 40, 44, 47 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) | 
| 49 | 21 | rprege0d 13084 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) | 
| 50 | 24, 25, 42 | nvsge0 30683 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅 · ((normCV‘𝑈)‘𝑥))) | 
| 51 | 18, 49, 23, 50 | syl3anc 1373 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅 · ((normCV‘𝑈)‘𝑥))) | 
| 52 | 48, 51 | eqtrd 2777 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = (𝑅 · ((normCV‘𝑈)‘𝑥))) | 
| 53 | 22 | mulridd 11278 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · 1) = 𝑅) | 
| 54 | 53 | eqcomd 2743 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 = (𝑅 · 1)) | 
| 55 | 52, 54 | breq12d 5156 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 ↔ (𝑅 · ((normCV‘𝑈)‘𝑥)) ≤ (𝑅 · 1))) | 
| 56 | 24, 42 | nvcl 30680 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) | 
| 57 | 17, 56 | mpan 690 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → ((normCV‘𝑈)‘𝑥) ∈ ℝ) | 
| 58 | 57 | adantl 481 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) | 
| 59 |  | 1red 11262 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℝ) | 
| 60 | 58, 59, 21 | lemul2d 13121 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 ↔ (𝑅 · ((normCV‘𝑈)‘𝑥)) ≤ (𝑅 · 1))) | 
| 61 | 55, 60 | bitr4d 282 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 ↔ ((normCV‘𝑈)‘𝑥) ≤ 1)) | 
| 62 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝐾)) | 
| 63 | 62 | ralbidv 3178 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾)) | 
| 64 | 63 | rabbidv 3444 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) | 
| 65 |  | ubthlem.9 | . . . . . . . . . . . 12
⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) | 
| 66 | 24 | fvexi 6920 | . . . . . . . . . . . . 13
⊢ 𝑋 ∈ V | 
| 67 | 66 | rabex 5339 | . . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ∈ V | 
| 68 | 64, 65, 67 | fvmpt 7016 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → (𝐴‘𝐾) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) | 
| 69 | 1, 68 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝐾) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) | 
| 70 | 69 | eleq2d 2827 | . . . . . . . . 9
⊢ (𝜑 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾})) | 
| 71 |  | 2fveq3 6911 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))))) | 
| 72 | 71 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → ((𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 73 | 72 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 74 | 73 | elrab 3692 | . . . . . . . . 9
⊢ ((𝑃( +𝑣
‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 75 | 70, 74 | bitrdi 287 | . . . . . . . 8
⊢ (𝜑 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) | 
| 76 | 75 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) | 
| 77 | 31, 61, 76 | 3imtr3d 293 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) | 
| 78 |  | rsp 3247 | . . . . . . . . . 10
⊢
(∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑡 ∈ 𝑇 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 79 | 78 | com12 32 | . . . . . . . . 9
⊢ (𝑡 ∈ 𝑇 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 80 | 79 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) | 
| 81 |  | xmet0 24352 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃𝐷𝑃) = 0) | 
| 82 | 37, 19, 81 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑃𝐷𝑃) = 0) | 
| 83 | 4 | rpge0d 13081 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 𝑅) | 
| 84 | 82, 83 | eqbrtrd 5165 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃𝐷𝑃) ≤ 𝑅) | 
| 85 |  | oveq2 7439 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑃 → (𝑃𝐷𝑧) = (𝑃𝐷𝑃)) | 
| 86 | 85 | breq1d 5153 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑃 → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷𝑃) ≤ 𝑅)) | 
| 87 | 86 | elrab 3692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ↔ (𝑃 ∈ 𝑋 ∧ (𝑃𝐷𝑃) ≤ 𝑅)) | 
| 88 | 19, 84, 87 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}) | 
| 89 | 11, 88 | sseldd 3984 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ (𝐴‘𝐾)) | 
| 90 | 89, 69 | eleqtrd 2843 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) | 
| 91 |  | 2fveq3 6911 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑃 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑃))) | 
| 92 | 91 | breq1d 5153 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑃 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) | 
| 93 | 92 | ralbidv 3178 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑃 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) | 
| 94 | 93 | elrab 3692 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) | 
| 95 | 90, 94 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) | 
| 96 | 95 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) | 
| 97 | 96 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) | 
| 98 | 97 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) | 
| 99 |  | ubthlem.6 | . . . . . . . . . . . . 13
⊢ 𝑊 ∈ NrmCVec | 
| 100 |  | ubthlem.7 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) | 
| 101 | 100 | sselda 3983 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) | 
| 102 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢
(IndMet‘𝑊) =
(IndMet‘𝑊) | 
| 103 |  | ubthlem.4 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 = (MetOpen‘𝐷) | 
| 104 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊)) | 
| 105 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) | 
| 106 | 32, 102, 103, 104, 105, 17, 99 | blocn2 30827 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊)))) | 
| 107 | 103 | mopntopon 24449 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 108 | 37, 107 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ∈ (TopOn‘𝑋) | 
| 109 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) | 
| 110 | 109, 102 | imsxmet 30711 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ NrmCVec →
(IndMet‘𝑊) ∈
(∞Met‘(BaseSet‘𝑊))) | 
| 111 | 104 | mopntopon 24449 | . . . . . . . . . . . . . . . . . . . 20
⊢
((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈
(TopOn‘(BaseSet‘𝑊))) | 
| 112 | 99, 110, 111 | mp2b 10 | . . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)) | 
| 113 |  | iscncl 23277 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))) | 
| 114 | 108, 112,
113 | mp2an 692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) | 
| 115 | 106, 114 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) | 
| 116 | 101, 115 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) | 
| 117 | 116 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑡:𝑋⟶(BaseSet‘𝑊)) | 
| 119 | 118, 30 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊)) | 
| 120 |  | ubth.2 | . . . . . . . . . . . . . 14
⊢ 𝑁 =
(normCV‘𝑊) | 
| 121 | 109, 120 | nvcl 30680 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ) | 
| 122 | 99, 119, 121 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ) | 
| 123 | 118, 20 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) | 
| 124 | 109, 120 | nvcl 30680 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑃)) ∈ ℝ) | 
| 125 | 99, 123, 124 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑃)) ∈ ℝ) | 
| 126 | 1 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 127 | 126 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ ℝ) | 
| 128 |  | le2add 11745 | . . . . . . . . . . . 12
⊢ ((((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ ∧ (𝑁‘(𝑡‘𝑃)) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ)) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) | 
| 129 | 122, 125,
127, 127, 128 | syl22anc 839 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) | 
| 130 | 98, 129 | mpan2d 694 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) | 
| 131 | 46 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) | 
| 132 | 99 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑊 ∈ NrmCVec) | 
| 133 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 LnOp 𝑊) = (𝑈 LnOp 𝑊) | 
| 134 | 133, 105 | bloln 30803 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 BLnOp 𝑊)) → 𝑡 ∈ (𝑈 LnOp 𝑊)) | 
| 135 | 17, 99, 134 | mp3an12 1453 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝑈 LnOp 𝑊)) | 
| 136 | 101, 135 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 LnOp 𝑊)) | 
| 137 | 136 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑡 ∈ (𝑈 LnOp 𝑊)) | 
| 138 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) | 
| 139 | 24, 41, 138, 133 | lnosub 30778 | . . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) | 
| 140 | 18, 132, 137, 30, 20, 139 | syl32anc 1380 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) | 
| 141 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) | 
| 142 | 24, 25, 141, 133 | lnomul 30779 | . . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ (𝑅 ∈ ℂ ∧ 𝑥 ∈ 𝑋)) → (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) | 
| 143 | 18, 132, 137, 22, 23, 142 | syl32anc 1380 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) | 
| 144 | 131, 140,
143 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) | 
| 145 | 144 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) = (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥)))) | 
| 146 | 117 | ffvelcdmda 7104 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) | 
| 147 | 109, 141,
120 | nvsge0 30683 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) | 
| 148 | 132, 49, 146, 147 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) | 
| 149 | 145, 148 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) | 
| 150 | 109, 138,
120 | nvmtri 30690 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊) ∧ (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) | 
| 151 | 132, 119,
123, 150 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) | 
| 152 | 149, 151 | eqbrtrrd 5167 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) | 
| 153 | 21 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈ ℝ) | 
| 154 | 109, 120 | nvcl 30680 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) | 
| 155 | 99, 146, 154 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) | 
| 156 | 153, 155 | remulcld 11291 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ∈ ℝ) | 
| 157 | 122, 125 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∈ ℝ) | 
| 158 | 3 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 𝐾) ∈ ℝ) | 
| 159 | 158 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝐾 + 𝐾) ∈ ℝ) | 
| 160 |  | letr 11355 | . . . . . . . . . . . 12
⊢ (((𝑅 · (𝑁‘(𝑡‘𝑥))) ∈ ℝ ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∈ ℝ ∧ (𝐾 + 𝐾) ∈ ℝ) → (((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) | 
| 161 | 156, 157,
159, 160 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) | 
| 162 | 152, 161 | mpand 695 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) | 
| 163 | 130, 162 | syld 47 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) | 
| 164 | 155, 159,
21 | lemuldiv2d 13127 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾) ↔ (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 165 | 163, 164 | sylibd 239 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 166 | 80, 165 | syld 47 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 167 | 166 | adantld 490 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾) → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 168 | 77, 167 | syld 47 | . . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 169 | 168 | ralrimiva 3146 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) | 
| 170 | 5 | rpxrd 13078 | . . . . . 6
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ*) | 
| 171 | 170 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ*) | 
| 172 |  | eqid 2737 | . . . . . 6
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) | 
| 173 | 24, 109, 42, 120, 172, 17, 99 | nmoubi 30791 | . . . . 5
⊢ ((𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*) →
(((𝑈 normOpOLD
𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))) | 
| 174 | 117, 171,
173 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))) | 
| 175 | 169, 174 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) | 
| 176 | 175 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) | 
| 177 |  | brralrspcev 5203 | . 2
⊢ ((((𝐾 + 𝐾) / 𝑅) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) | 
| 178 | 6, 176, 177 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |