Proof of Theorem ubthlem2
Step | Hyp | Ref
| Expression |
1 | | ubthlem.10 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
2 | 1 | nnrpd 11746 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
3 | 2, 2 | rpaddcld 11763 |
. . . 4
⊢ (𝜑 → (𝐾 + 𝐾) ∈
ℝ+) |
4 | | ubthlem.12 |
. . . 4
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
5 | 3, 4 | rpdivcld 11765 |
. . 3
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ+) |
6 | 5 | rpred 11748 |
. 2
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈ ℝ) |
7 | | ubthlem.13 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾)) |
8 | | rabss 3642 |
. . . . . . . . . 10
⊢ ({𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾) ↔ ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) |
9 | 7, 8 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) |
10 | 9 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ∀𝑧 ∈ 𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾))) |
11 | | ubthlem.5 |
. . . . . . . . . . 11
⊢ 𝑈 ∈ CBan |
12 | | bnnv 27106 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ CBan → 𝑈 ∈
NrmCVec) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑈 ∈ NrmCVec |
14 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑈 ∈ NrmCVec) |
15 | | ubthlem.11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
16 | 15 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑃 ∈ 𝑋) |
17 | 4 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈
ℝ+) |
18 | 17 | rpcnd 11750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈ ℂ) |
19 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
20 | | ubth.1 |
. . . . . . . . . . 11
⊢ 𝑋 = (BaseSet‘𝑈) |
21 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
22 | 20, 21 | nvscl 26865 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑅 ∈ ℂ ∧ 𝑥 ∈ 𝑋) → (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) |
23 | 14, 18, 19, 22 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
25 | 20, 24 | nvgcl 26859 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) |
26 | 14, 16, 23, 25 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) |
27 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑃𝐷𝑧) = (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) |
28 | 27 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅)) |
29 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑧 ∈ (𝐴‘𝐾) ↔ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾))) |
30 | 28, 29 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾)) ↔ ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾)))) |
31 | 30 | rspccv 3279 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝑋 ((𝑃𝐷𝑧) ≤ 𝑅 → 𝑧 ∈ (𝐴‘𝐾)) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾)))) |
32 | 10, 26, 31 | sylc 63 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 → (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾))) |
33 | | ubthlem.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝐷 = (IndMet‘𝑈) |
34 | 20, 33 | cbncms 27105 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) |
35 | 11, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈ (CMet‘𝑋) |
36 | | cmetmet 22892 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
37 | | metxmet 21949 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
38 | 35, 36, 37 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ (∞Met‘𝑋) |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
40 | | xmetsym 21962 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃)) |
41 | 39, 16, 26, 40 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃)) |
42 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) |
43 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
44 | 20, 42, 43, 33 | imsdval 26925 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑃( +𝑣
‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃))) |
45 | 14, 26, 16, 44 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))𝐷𝑃) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃))) |
46 | 20, 24, 42 | nvpncan2 26892 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ (𝑅( ·𝑠OLD
‘𝑈)𝑥) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃) = (𝑅( ·𝑠OLD
‘𝑈)𝑥)) |
47 | 14, 16, 23, 46 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃) = (𝑅( ·𝑠OLD
‘𝑈)𝑥)) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) |
49 | 41, 45, 48 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) |
50 | 17 | rprege0d 11755 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) |
51 | 20, 21, 43 | nvsge0 26903 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅 · ((normCV‘𝑈)‘𝑥))) |
52 | 14, 50, 19, 51 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅 · ((normCV‘𝑈)‘𝑥))) |
53 | 49, 52 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) = (𝑅 · ((normCV‘𝑈)‘𝑥))) |
54 | 18 | mulid1d 9936 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · 1) = 𝑅) |
55 | 54 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 = (𝑅 · 1)) |
56 | 53, 55 | breq12d 4596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 ↔ (𝑅 · ((normCV‘𝑈)‘𝑥)) ≤ (𝑅 · 1))) |
57 | 20, 43 | nvcl 26900 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
58 | 13, 57 | mpan 702 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
59 | 58 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
60 | | 1red 9934 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 1 ∈ ℝ) |
61 | 59, 60, 17 | lemul2d 11792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 ↔ (𝑅 · ((normCV‘𝑈)‘𝑥)) ≤ (𝑅 · 1))) |
62 | 56, 61 | bitr4d 270 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃𝐷(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ≤ 𝑅 ↔ ((normCV‘𝑈)‘𝑥) ≤ 1)) |
63 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝐾)) |
64 | 63 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾)) |
65 | 64 | rabbidv 3164 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) |
66 | | ubthlem.9 |
. . . . . . . . . . . 12
⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
67 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(BaseSet‘𝑈)
∈ V |
68 | 20, 67 | eqeltri 2684 |
. . . . . . . . . . . . 13
⊢ 𝑋 ∈ V |
69 | 68 | rabex 4740 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ∈ V |
70 | 65, 66, 69 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → (𝐴‘𝐾) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) |
71 | 1, 70 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝐾) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) |
72 | 71 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾})) |
73 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑡‘𝑧) = (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) |
74 | 73 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))))) |
75 | 74 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → ((𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
76 | 75 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
77 | 76 | elrab 3331 |
. . . . . . . . 9
⊢ ((𝑃( +𝑣
‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
78 | 72, 77 | syl6bb 275 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) |
79 | 78 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ (𝐴‘𝐾) ↔ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) |
80 | 32, 62, 79 | 3imtr3d 281 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 → ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾))) |
81 | | rsp 2913 |
. . . . . . . . . 10
⊢
(∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑡 ∈ 𝑇 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
82 | 81 | com12 32 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝑇 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
83 | 82 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾)) |
84 | | xmet0 21957 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃𝐷𝑃) = 0) |
85 | 38, 15, 84 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑃𝐷𝑃) = 0) |
86 | 4 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 𝑅) |
87 | 85, 86 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃𝐷𝑃) ≤ 𝑅) |
88 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑃 → (𝑃𝐷𝑧) = (𝑃𝐷𝑃)) |
89 | 88 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑃 → ((𝑃𝐷𝑧) ≤ 𝑅 ↔ (𝑃𝐷𝑃) ≤ 𝑅)) |
90 | 89 | elrab 3331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ↔ (𝑃 ∈ 𝑋 ∧ (𝑃𝐷𝑃) ≤ 𝑅)) |
91 | 15, 87, 90 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}) |
92 | 7, 91 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ (𝐴‘𝐾)) |
93 | 92, 71 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾}) |
94 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑃 → (𝑡‘𝑧) = (𝑡‘𝑃)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑃 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑃))) |
96 | 95 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑃 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) |
97 | 96 | ralbidv 2969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑃 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) |
98 | 97 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝐾} ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) |
99 | 93, 98 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾)) |
100 | 99 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) |
101 | 100 | r19.21bi 2916 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) |
102 | 101 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) |
103 | | ubthlem.6 |
. . . . . . . . . . . . 13
⊢ 𝑊 ∈ NrmCVec |
104 | | ubthlem.7 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
105 | 104 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
106 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(IndMet‘𝑊) =
(IndMet‘𝑊) |
107 | | ubthlem.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 = (MetOpen‘𝐷) |
108 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊)) |
109 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) |
110 | 33, 106, 107, 108, 109, 13, 103 | blocn2 27047 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊)))) |
111 | 107 | mopntopon 22054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
112 | 38, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ∈ (TopOn‘𝑋) |
113 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
114 | 113, 106 | imsxmet 26931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ NrmCVec →
(IndMet‘𝑊) ∈
(∞Met‘(BaseSet‘𝑊))) |
115 | 108 | mopntopon 22054 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈
(TopOn‘(BaseSet‘𝑊))) |
116 | 103, 114,
115 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)) |
117 | | iscncl 20883 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))) |
118 | 112, 116,
117 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
119 | 110, 118 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
120 | 105, 119 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
121 | 120 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
123 | 122, 26 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊)) |
124 | | ubth.2 |
. . . . . . . . . . . . . 14
⊢ 𝑁 =
(normCV‘𝑊) |
125 | 113, 124 | nvcl 26900 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ) |
126 | 103, 123,
125 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ) |
127 | 122, 16 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) |
128 | 113, 124 | nvcl 26900 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑃)) ∈ ℝ) |
129 | 103, 127,
128 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑃)) ∈ ℝ) |
130 | 1 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℝ) |
131 | 130 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ ℝ) |
132 | | le2add 10389 |
. . . . . . . . . . . 12
⊢ ((((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ∈ ℝ ∧ (𝑁‘(𝑡‘𝑃)) ∈ ℝ) ∧ (𝐾 ∈ ℝ ∧ 𝐾 ∈ ℝ)) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) |
133 | 126, 129,
131, 131, 132 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 ∧ (𝑁‘(𝑡‘𝑃)) ≤ 𝐾) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) |
134 | 102, 133 | mpan2d 706 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾))) |
135 | 47 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥))) |
136 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑊 ∈ NrmCVec) |
137 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 LnOp 𝑊) = (𝑈 LnOp 𝑊) |
138 | 137, 109 | bloln 27023 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 BLnOp 𝑊)) → 𝑡 ∈ (𝑈 LnOp 𝑊)) |
139 | 13, 103, 138 | mp3an12 1406 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝑈 LnOp 𝑊)) |
140 | 105, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 LnOp 𝑊)) |
141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑡 ∈ (𝑈 LnOp 𝑊)) |
142 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) |
143 | 20, 42, 142, 137 | lnosub 26998 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ ((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) |
144 | 14, 136, 141, 26, 16, 143 | syl32anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))( −𝑣 ‘𝑈)𝑃)) = ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) |
145 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
146 | 20, 21, 145, 137 | lnomul 26999 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 LnOp 𝑊)) ∧ (𝑅 ∈ ℂ ∧ 𝑥 ∈ 𝑋)) → (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) |
147 | 14, 136, 141, 18, 19, 146 | syl32anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘(𝑅( ·𝑠OLD
‘𝑈)𝑥)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) |
148 | 135, 144,
147 | 3eqtr3d 2652 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃)) = (𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) |
149 | 148 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) = (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥)))) |
150 | 121 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
151 | 113, 145,
124 | nvsge0 26903 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑅 ∈ ℝ ∧ 0 ≤
𝑅) ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) |
152 | 136, 50, 150, 151 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑅( ·𝑠OLD
‘𝑊)(𝑡‘𝑥))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) |
153 | 149, 152 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) = (𝑅 · (𝑁‘(𝑡‘𝑥)))) |
154 | 113, 142,
124 | nvmtri 26910 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥))) ∈ (BaseSet‘𝑊) ∧ (𝑡‘𝑃) ∈ (BaseSet‘𝑊)) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) |
155 | 136, 123,
127, 154 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘((𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))( −𝑣 ‘𝑊)(𝑡‘𝑃))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) |
156 | 153, 155 | eqbrtrrd 4607 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃)))) |
157 | 17 | rpred 11748 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → 𝑅 ∈ ℝ) |
158 | 113, 124 | nvcl 26900 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
159 | 103, 150,
158 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
160 | 157, 159 | remulcld 9949 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ∈ ℝ) |
161 | 126, 129 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∈ ℝ) |
162 | 3 | rpred 11748 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 𝐾) ∈ ℝ) |
163 | 162 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝐾 + 𝐾) ∈ ℝ) |
164 | | letr 10010 |
. . . . . . . . . . . 12
⊢ (((𝑅 · (𝑁‘(𝑡‘𝑥))) ∈ ℝ ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∈ ℝ ∧ (𝐾 + 𝐾) ∈ ℝ) → (((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) |
165 | 160, 161,
163, 164 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ∧ ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾)) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) |
166 | 156, 165 | mpand 707 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) + (𝑁‘(𝑡‘𝑃))) ≤ (𝐾 + 𝐾) → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) |
167 | 134, 166 | syld 46 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾))) |
168 | 159, 163,
17 | lemuldiv2d 11798 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑅 · (𝑁‘(𝑡‘𝑥))) ≤ (𝐾 + 𝐾) ↔ (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
169 | 167, 168 | sylibd 228 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
170 | 83, 169 | syld 46 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
171 | 170 | adantld 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)) ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘(𝑃( +𝑣 ‘𝑈)(𝑅( ·𝑠OLD
‘𝑈)𝑥)))) ≤ 𝐾) → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
172 | 80, 171 | syld 46 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
173 | 172 | ralrimiva 2949 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅))) |
174 | 5 | rpxrd 11749 |
. . . . . 6
⊢ (𝜑 → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ*) |
175 | 174 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐾 + 𝐾) / 𝑅) ∈
ℝ*) |
176 | | eqid 2610 |
. . . . . 6
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) |
177 | 20, 113, 43, 124, 176, 13, 103 | nmoubi 27011 |
. . . . 5
⊢ ((𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ((𝐾 + 𝐾) / 𝑅) ∈ ℝ*) →
(((𝑈 normOpOLD
𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))) |
178 | 121, 175,
177 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘𝑥) ≤ 1 → (𝑁‘(𝑡‘𝑥)) ≤ ((𝐾 + 𝐾) / 𝑅)))) |
179 | 173, 178 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) |
180 | 179 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) |
181 | | breq2 4587 |
. . . 4
⊢ (𝑑 = ((𝐾 + 𝐾) / 𝑅) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))) |
182 | 181 | ralbidv 2969 |
. . 3
⊢ (𝑑 = ((𝐾 + 𝐾) / 𝑅) → (∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅))) |
183 | 182 | rspcev 3282 |
. 2
⊢ ((((𝐾 + 𝐾) / 𝑅) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ ((𝐾 + 𝐾) / 𝑅)) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |
184 | 6, 180, 183 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |