Metamath Proof Explorer


Theorem smcnlem

Description: Lemma for smcn . (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Hypotheses smcn.c 𝐶 = ( IndMet ‘ 𝑈 )
smcn.j 𝐽 = ( MetOpen ‘ 𝐶 )
smcn.s 𝑆 = ( ·𝑠OLD𝑈 )
smcn.k 𝐾 = ( TopOpen ‘ ℂfld )
smcn.x 𝑋 = ( BaseSet ‘ 𝑈 )
smcn.n 𝑁 = ( normCV𝑈 )
smcn.u 𝑈 ∈ NrmCVec
smcn.t 𝑇 = ( 1 / ( 1 + ( ( ( ( 𝑁𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) )
Assertion smcnlem 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )

Proof

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 𝐽 )