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
|
syl6bb |
⊢ ( 𝜑 → ( ( 𝑃 ( +𝑣 ‘ 𝑈 ) ( 𝑅 ( ·𝑠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 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) |