Step |
Hyp |
Ref |
Expression |
1 |
|
smcn.c |
⊢ 𝐶 = ( IndMet ‘ 𝑈 ) |
2 |
|
smcn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) |
3 |
|
smcn.s |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
smcn.k |
⊢ 𝐾 = ( TopOpen ‘ ℂfld ) |
5 |
|
smcn.x |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
6 |
|
smcn.n |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
7 |
|
smcn.u |
⊢ 𝑈 ∈ NrmCVec |
8 |
|
smcn.t |
⊢ 𝑇 = ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
9 |
5 3
|
nvsf |
⊢ ( 𝑈 ∈ NrmCVec → 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ) |
10 |
7 9
|
ax-mp |
⊢ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 |
11 |
|
1rp |
⊢ 1 ∈ ℝ+ |
12 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 ) |
13 |
5 6
|
nvcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) |
14 |
7 12 13
|
sylancr |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) |
15 |
|
abscl |
⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ ) |
16 |
15
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( abs ‘ 𝑥 ) ∈ ℝ ) |
17 |
14 16
|
readdcld |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ ) |
18 |
5 6
|
nvge0 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) ) |
19 |
7 12 18
|
sylancr |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) ) |
20 |
|
absge0 |
⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( abs ‘ 𝑥 ) ) |
21 |
20
|
adantr |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( abs ‘ 𝑥 ) ) |
22 |
14 16 19 21
|
addge0d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ) |
23 |
17 22
|
ge0p1rpd |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ+ ) |
24 |
|
rpdivcl |
⊢ ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ+ ∧ 𝑟 ∈ ℝ+ ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) |
25 |
23 24
|
sylan |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) |
26 |
|
rpaddcl |
⊢ ( ( 1 ∈ ℝ+ ∧ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ ) |
27 |
11 25 26
|
sylancr |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ ) |
28 |
27
|
rpreccld |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ∈ ℝ+ ) |
29 |
8 28
|
eqeltrid |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → 𝑇 ∈ ℝ+ ) |
30 |
5 1
|
imsmet |
⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( Met ‘ 𝑋 ) ) |
31 |
7 30
|
ax-mp |
⊢ 𝐶 ∈ ( Met ‘ 𝑋 ) |
32 |
31
|
a1i |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝐶 ∈ ( Met ‘ 𝑋 ) ) |
33 |
7
|
a1i |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑈 ∈ NrmCVec ) |
34 |
|
simplll |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑥 ∈ ℂ ) |
35 |
|
simpllr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑦 ∈ 𝑋 ) |
36 |
5 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ) |
37 |
33 34 35 36
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ) |
38 |
|
simprll |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑧 ∈ ℂ ) |
39 |
|
simprlr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑤 ∈ 𝑋 ) |
40 |
5 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) |
41 |
33 38 39 40
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) |
42 |
|
metcl |
⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ ) |
43 |
32 37 41 42
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ ) |
44 |
5 3
|
nvscl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) |
45 |
33 38 35 44
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) |
46 |
|
metcl |
⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) ∈ ℝ ) |
47 |
32 37 45 46
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) ∈ ℝ ) |
48 |
|
metcl |
⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ ) |
49 |
32 45 41 48
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ∈ ℝ ) |
50 |
47 49
|
readdcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ∈ ℝ ) |
51 |
|
rpre |
⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ ) |
52 |
51
|
ad2antlr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑟 ∈ ℝ ) |
53 |
|
mettri |
⊢ ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ ( ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ≤ ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ) |
54 |
32 37 41 45 53
|
syl13anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ≤ ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ) |
55 |
7 35 13
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℝ ) |
56 |
34
|
abscld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ ) |
57 |
55 56
|
readdcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ ) |
58 |
|
peano2re |
⊢ ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) ∈ ℝ → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ ) |
59 |
57 58
|
syl |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℝ ) |
60 |
29
|
adantr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℝ+ ) |
61 |
60
|
rpred |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℝ ) |
62 |
59 61
|
remulcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) ∈ ℝ ) |
63 |
34 38
|
subcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℂ ) |
64 |
63
|
abscld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) ∈ ℝ ) |
65 |
64 55
|
remulcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ∈ ℝ ) |
66 |
38
|
abscld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ∈ ℝ ) |
67 |
|
eqid |
⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 ) |
68 |
5 67
|
nvmcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) |
69 |
33 35 39 68
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) |
70 |
5 6
|
nvcl |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ∈ ℝ ) |
71 |
7 69 70
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ∈ ℝ ) |
72 |
66 71
|
remulcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ∈ ℝ ) |
73 |
55 61
|
remulcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) ∈ ℝ ) |
74 |
|
peano2re |
⊢ ( ( abs ‘ 𝑥 ) ∈ ℝ → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℝ ) |
75 |
56 74
|
syl |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℝ ) |
76 |
75 61
|
remulcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ∈ ℝ ) |
77 |
7 35 18
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( 𝑁 ‘ 𝑦 ) ) |
78 |
34 38
|
abssubd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) ) |
79 |
38 34
|
subcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 − 𝑥 ) ∈ ℂ ) |
80 |
79
|
abscld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ∈ ℝ ) |
81 |
|
eqid |
⊢ ( abs ∘ − ) = ( abs ∘ − ) |
82 |
81
|
cnmetdval |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) ) |
83 |
34 38 82
|
syl2anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑥 − 𝑧 ) ) ) |
84 |
83 78
|
eqtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) = ( abs ‘ ( 𝑧 − 𝑥 ) ) ) |
85 |
|
simprrl |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ) |
86 |
84 85
|
eqbrtrrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) < 𝑇 ) |
87 |
80 61 86
|
ltled |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ≤ 𝑇 ) |
88 |
78 87
|
eqbrtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 − 𝑧 ) ) ≤ 𝑇 ) |
89 |
64 61 55 77 88
|
lemul1ad |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( 𝑇 · ( 𝑁 ‘ 𝑦 ) ) ) |
90 |
60
|
rpcnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ∈ ℂ ) |
91 |
55
|
recnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ 𝑦 ) ∈ ℂ ) |
92 |
90 91
|
mulcomd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑇 · ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) ) |
93 |
89 92
|
breqtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) ) |
94 |
38
|
absge0d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( abs ‘ 𝑧 ) ) |
95 |
5 6
|
nvge0 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) |
96 |
7 69 95
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 0 ≤ ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) |
97 |
56 80
|
readdcld |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ∈ ℝ ) |
98 |
34 38
|
pncan3d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( 𝑧 − 𝑥 ) ) = 𝑧 ) |
99 |
98
|
fveq2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) = ( abs ‘ 𝑧 ) ) |
100 |
34 79
|
abstrid |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑥 + ( 𝑧 − 𝑥 ) ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ) |
101 |
99 100
|
eqbrtrrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ) |
102 |
|
1red |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 ∈ ℝ ) |
103 |
|
1re |
⊢ 1 ∈ ℝ |
104 |
25
|
adantr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) |
105 |
|
ltaddrp |
⊢ ( ( 1 ∈ ℝ ∧ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ+ ) → 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
106 |
103 104 105
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
107 |
27
|
adantr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℝ+ ) |
108 |
107
|
recgt1d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ↔ ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 1 ) ) |
109 |
106 108
|
mpbid |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 1 ) |
110 |
8 109
|
eqbrtrid |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 < 1 ) |
111 |
61 102 110
|
ltled |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑇 ≤ 1 ) |
112 |
80 61 102 87 111
|
letrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ ( 𝑧 − 𝑥 ) ) ≤ 1 ) |
113 |
80 102 56 112
|
leadd2dd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + ( abs ‘ ( 𝑧 − 𝑥 ) ) ) ≤ ( ( abs ‘ 𝑥 ) + 1 ) ) |
114 |
66 97 75 101 113
|
letrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑧 ) ≤ ( ( abs ‘ 𝑥 ) + 1 ) ) |
115 |
5 67 6 1
|
imsdval |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 𝐶 𝑤 ) = ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) |
116 |
33 35 39 115
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 𝐶 𝑤 ) = ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) |
117 |
|
simprrr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑦 𝐶 𝑤 ) < 𝑇 ) |
118 |
116 117
|
eqbrtrrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) < 𝑇 ) |
119 |
71 61 118
|
ltled |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ≤ 𝑇 ) |
120 |
66 75 71 61 94 96 114 119
|
lemul12ad |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ≤ ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) |
121 |
65 72 73 76 93 120
|
le2addd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) + ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) ≤ ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) ) |
122 |
|
eqid |
⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 ) |
123 |
5 122 3 6 1
|
imsdval2 |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) ) |
124 |
33 37 45 123
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) ) |
125 |
|
neg1cn |
⊢ - 1 ∈ ℂ |
126 |
|
mulcl |
⊢ ( ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 1 · 𝑧 ) ∈ ℂ ) |
127 |
125 38 126
|
sylancr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( - 1 · 𝑧 ) ∈ ℂ ) |
128 |
5 122 3
|
nvdir |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ℂ ∧ ( - 1 · 𝑧 ) ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) ) |
129 |
33 34 127 35 128
|
syl13anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) ) |
130 |
38
|
mulm1d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( - 1 · 𝑧 ) = - 𝑧 ) |
131 |
130
|
oveq2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( - 1 · 𝑧 ) ) = ( 𝑥 + - 𝑧 ) ) |
132 |
34 38
|
negsubd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + - 𝑧 ) = ( 𝑥 − 𝑧 ) ) |
133 |
131 132
|
eqtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑥 + ( - 1 · 𝑧 ) ) = ( 𝑥 − 𝑧 ) ) |
134 |
133
|
oveq1d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 + ( - 1 · 𝑧 ) ) 𝑆 𝑦 ) = ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) |
135 |
125
|
a1i |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → - 1 ∈ ℂ ) |
136 |
5 3
|
nvsass |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ) → ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) = ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) |
137 |
33 135 38 35 136
|
syl13anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) = ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) |
138 |
137
|
oveq2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( ( - 1 · 𝑧 ) 𝑆 𝑦 ) ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) |
139 |
129 134 138
|
3eqtr3d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) = ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) |
140 |
139
|
fveq2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( 𝑁 ‘ ( ( 𝑥 𝑆 𝑦 ) ( +𝑣 ‘ 𝑈 ) ( - 1 𝑆 ( 𝑧 𝑆 𝑦 ) ) ) ) ) |
141 |
5 3 6
|
nvs |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 − 𝑧 ) ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ) |
142 |
33 63 35 141
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( ( 𝑥 − 𝑧 ) 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ) |
143 |
124 140 142
|
3eqtr2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) = ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) ) |
144 |
5 67 6 1
|
imsdval |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑧 𝑆 𝑦 ) ∈ 𝑋 ∧ ( 𝑧 𝑆 𝑤 ) ∈ 𝑋 ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) ) |
145 |
33 45 41 144
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) ) |
146 |
5 67 3
|
nvmdi |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) |
147 |
33 38 35 39 146
|
syl13anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) = ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) |
148 |
147
|
fveq2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( 𝑁 ‘ ( ( 𝑧 𝑆 𝑦 ) ( −𝑣 ‘ 𝑈 ) ( 𝑧 𝑆 𝑤 ) ) ) ) |
149 |
5 3 6
|
nvs |
⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) |
150 |
33 38 69 149
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 𝑁 ‘ ( 𝑧 𝑆 ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) |
151 |
145 148 150
|
3eqtr2d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) = ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) |
152 |
143 151
|
oveq12d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) = ( ( ( abs ‘ ( 𝑥 − 𝑧 ) ) · ( 𝑁 ‘ 𝑦 ) ) + ( ( abs ‘ 𝑧 ) · ( 𝑁 ‘ ( 𝑦 ( −𝑣 ‘ 𝑈 ) 𝑤 ) ) ) ) ) |
153 |
56
|
recnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℂ ) |
154 |
|
1cnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 1 ∈ ℂ ) |
155 |
91 153 154
|
addassd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) = ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) ) |
156 |
155
|
oveq1d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) · 𝑇 ) ) |
157 |
75
|
recnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( abs ‘ 𝑥 ) + 1 ) ∈ ℂ ) |
158 |
91 157 90
|
adddird |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( ( abs ‘ 𝑥 ) + 1 ) ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) ) |
159 |
156 158
|
eqtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( 𝑁 ‘ 𝑦 ) · 𝑇 ) + ( ( ( abs ‘ 𝑥 ) + 1 ) · 𝑇 ) ) ) |
160 |
121 152 159
|
3brtr4d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) ≤ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) ) |
161 |
8
|
oveq2i |
⊢ ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ) |
162 |
59
|
recnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) ∈ ℂ ) |
163 |
107
|
rpcnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ∈ ℂ ) |
164 |
107
|
rpne0d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ≠ 0 ) |
165 |
162 163 164
|
divrecd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · ( 1 / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ) ) |
166 |
161 165
|
eqtr4id |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) = ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) ) |
167 |
|
simplr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → 𝑟 ∈ ℝ+ ) |
168 |
104
|
rpred |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℝ ) |
169 |
168
|
ltp1d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) < ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) + 1 ) ) |
170 |
104
|
rpcnd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ∈ ℂ ) |
171 |
170 154
|
addcomd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) + 1 ) = ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
172 |
169 171
|
breqtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) < ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
173 |
59 167 107 172
|
ltdiv23d |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / ( 1 + ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) < 𝑟 ) |
174 |
166 173
|
eqbrtrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( ( 𝑁 ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) · 𝑇 ) < 𝑟 ) |
175 |
50 62 52 160 174
|
lelttrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑦 ) ) + ( ( 𝑧 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) ) < 𝑟 ) |
176 |
43 50 52 54 175
|
lelttrd |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) |
177 |
176
|
expr |
⊢ ( ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) |
178 |
177
|
ralrimivva |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) |
179 |
|
breq2 |
⊢ ( 𝑠 = 𝑇 → ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ↔ ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ) ) |
180 |
|
breq2 |
⊢ ( 𝑠 = 𝑇 → ( ( 𝑦 𝐶 𝑤 ) < 𝑠 ↔ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) |
181 |
179 180
|
anbi12d |
⊢ ( 𝑠 = 𝑇 → ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) ) ) |
182 |
181
|
imbi1d |
⊢ ( 𝑠 = 𝑇 → ( ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) ) |
183 |
182
|
2ralbidv |
⊢ ( 𝑠 = 𝑇 → ( ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) ) |
184 |
183
|
rspcev |
⊢ ( ( 𝑇 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑇 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑇 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) |
185 |
29 178 184
|
syl2anc |
⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) |
186 |
185
|
ralrimiva |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) |
187 |
186
|
rgen2 |
⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) |
188 |
|
cnxmet |
⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) |
189 |
5 1
|
imsxmet |
⊢ ( 𝑈 ∈ NrmCVec → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) |
190 |
7 189
|
ax-mp |
⊢ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) |
191 |
4
|
cnfldtopn |
⊢ 𝐾 = ( MetOpen ‘ ( abs ∘ − ) ) |
192 |
191 2 2
|
txmetcn |
⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) ) ) |
193 |
188 190 190 192
|
mp3an |
⊢ ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 ( abs ∘ − ) 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐶 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝑆 𝑦 ) 𝐶 ( 𝑧 𝑆 𝑤 ) ) < 𝑟 ) ) ) |
194 |
10 187 193
|
mpbir2an |
⊢ 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) |