smcnlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > smcnlem		Structured version Visualization version GIF version

Theorem smcnlem 27552

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

**Hypotheses**
Ref	Expression
smcn.c	⊢ 𝐶 = (IndMet‘𝑈)
smcn.j	⊢ 𝐽 = (MetOpen‘𝐶)
smcn.s	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
smcn.k	⊢ 𝐾 = (TopOpen‘ℂ_fld)
smcn.x	⊢ 𝑋 = (BaseSet‘𝑈)
smcn.n	⊢ 𝑁 = (norm_CV‘𝑈)
smcn.u	⊢ 𝑈 ∈ NrmCVec
smcn.t	⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))

**Assertion**
Ref	Expression
smcnlem	⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Distinct variable groups: 𝑥,𝑟,𝑦,𝐶 𝐽,𝑟,𝑥,𝑦 𝑈,𝑟,𝑥,𝑦 𝐾,𝑟,𝑥,𝑦 𝑆,𝑟,𝑥,𝑦 𝑋,𝑟,𝑥,𝑦 Allowed substitution hints: 𝑇(𝑥,𝑦,𝑟) 𝑁(𝑥,𝑦,𝑟)

Proof of Theorem smcnlem Dummy variables 𝑠 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		smcn.u	. . 3 ⊢ 𝑈 ∈ NrmCVec
2		smcn.x	. . . 4 ⊢ 𝑋 = (BaseSet‘𝑈)
3		smcn.s	. . . 4 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
4	2, 3	nvsf 27474	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
5	1, 4	ax-mp 5	. 2 ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋
6		smcn.t	. . . . . 6 ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
7		1rp 11836	. . . . . . . 8 ⊢ 1 ∈ ℝ⁺
8		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
9		smcn.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (norm_CV‘𝑈)
10	2, 9	nvcl 27516	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
11	1, 8, 10	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
12		abscl 14018	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
13	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
14	11, 13	readdcld 10069	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
15	2, 9	nvge0 27528	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
16	1, 8, 15	sylancr 695	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
17		absge0 14027	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 0 ≤ (abs‘𝑥))
18	17	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
19	11, 13, 16, 18	addge0d 10603	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ ((𝑁‘𝑦) + (abs‘𝑥)))
20	14, 19	ge0p1rpd 11902	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺)
21		rpdivcl 11856	. . . . . . . . 9 ⊢ (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
22	20, 21	sylan 488	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
23		rpaddcl 11854	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
24	7, 22, 23	sylancr 695	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
25	24	rpreccld 11882	. . . . . 6 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ∈ ℝ⁺)
26	6, 25	syl5eqel 2705	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
27		smcn.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (IndMet‘𝑈)
28	2, 27	imsmet 27546	. . . . . . . . . . 11 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (Met‘𝑋))
29	1, 28	ax-mp 5	. . . . . . . . . 10 ⊢ 𝐶 ∈ (Met‘𝑋)
30	29	a1i 11	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝐶 ∈ (Met‘𝑋))
31	1	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑈 ∈ NrmCVec)
32		simplll 798	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑥 ∈ ℂ)
33		simpllr 799	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑦 ∈ 𝑋)
34	2, 3	nvscl 27481	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑥𝑆𝑦) ∈ 𝑋)
35	31, 32, 33, 34	syl3anc 1326	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥𝑆𝑦) ∈ 𝑋)
36		simprll 802	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑧 ∈ ℂ)
37		simprlr 803	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑤 ∈ 𝑋)
38	2, 3	nvscl 27481	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) → (𝑧𝑆𝑤) ∈ 𝑋)
39	31, 36, 37, 38	syl3anc 1326	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑤) ∈ 𝑋)
40		metcl 22137	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
41	30, 35, 39, 40	syl3anc 1326	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
42	2, 3	nvscl 27481	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑧𝑆𝑦) ∈ 𝑋)
43	31, 36, 33, 42	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑦) ∈ 𝑋)
44		metcl 22137	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
45	30, 35, 43, 44	syl3anc 1326	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
46		metcl 22137	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
47	30, 43, 39, 46	syl3anc 1326	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
48	45, 47	readdcld 10069	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ∈ ℝ)
49		rpre 11839	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
50	49	ad2antlr 763	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ)
51		mettri 22157	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ ((𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋)) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
52	30, 35, 39, 43, 51	syl13anc 1328	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
53	1, 33, 10	sylancr 695	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℝ)
54	32	abscld 14175	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℝ)
55	53, 54	readdcld 10069	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
56		peano2re 10209	. . . . . . . . . . 11 ⊢ (((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
58	26	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ⁺)
59	58	rpred 11872	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ)
60	57, 59	remulcld 10070	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) ∈ ℝ)
61	32, 36	subcld 10392	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 − 𝑧) ∈ ℂ)
62	61	abscld 14175	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ∈ ℝ)
63	62, 53	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ∈ ℝ)
64	36	abscld 14175	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ∈ ℝ)
65		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ( −_𝑣 ‘𝑈) = ( −_𝑣 ‘𝑈)
66	2, 65	nvmcl 27501	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
67	31, 33, 37, 66	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
68	2, 9	nvcl 27516	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
69	1, 67, 68	sylancr 695	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
70	64, 69	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ∈ ℝ)
71	53, 59	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) · 𝑇) ∈ ℝ)
72		peano2re 10209	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
73	54, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℝ)
74	73, 59	remulcld 10070	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘𝑥) + 1) · 𝑇) ∈ ℝ)
75	1, 33, 15	sylancr 695	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘𝑦))
76	32, 36	abssubd 14192	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) = (abs‘(𝑧 − 𝑥)))
77	36, 32	subcld 10392	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧 − 𝑥) ∈ ℂ)
78	77	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ∈ ℝ)
79		eqid 2622	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 22574	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
81	32, 36, 80	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
82	81, 76	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑧 − 𝑥)))
83		simprrl 804	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) < 𝑇)
84	82, 83	eqbrtrrd 4677	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) < 𝑇)
85	78, 59, 84	ltled 10185	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 𝑇)
86	76, 85	eqbrtrd 4675	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ≤ 𝑇)
87	62, 59, 53, 75, 86	lemul1ad 10963	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ (𝑇 · (𝑁‘𝑦)))
88	58	rpcnd 11874	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℂ)
89	53	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℂ)
90	88, 89	mulcomd 10061	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑇 · (𝑁‘𝑦)) = ((𝑁‘𝑦) · 𝑇))
91	87, 90	breqtrd 4679	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ ((𝑁‘𝑦) · 𝑇))
92	36	absge0d 14183	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (abs‘𝑧))
93	2, 9	nvge0 27528	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
94	1, 67, 93	sylancr 695	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
95	54, 78	readdcld 10069	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ∈ ℝ)
96	32, 36	pncan3d 10395	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
97	96	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) = (abs‘𝑧))
98	32, 77	abstrid 14195	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
99	97, 98	eqbrtrrd 4677	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
100		1red 10055	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℝ)
101		1re 10039	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
102	22	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
103		ltaddrp 11867	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
104	101, 102, 103	sylancr 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
105	24	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
106	105	recgt1d 11886	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ↔ (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1))
107	104, 106	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1)
108	6, 107	syl5eqbr 4688	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 < 1)
109	59, 100, 108	ltled 10185	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ≤ 1)
110	78, 59, 100, 85, 109	letrd 10194	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 1)
111	78, 100, 54, 110	leadd2dd 10642	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ≤ ((abs‘𝑥) + 1))
112	64, 95, 73, 99, 111	letrd 10194	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + 1))
113	2, 65, 9, 27	imsdval 27541	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
114	31, 33, 37, 113	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
115		simprrr 805	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) < 𝑇)
116	114, 115	eqbrtrrd 4677	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) < 𝑇)
117	69, 59, 116	ltled 10185	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ≤ 𝑇)
118	64, 73, 69, 59, 92, 94, 112, 117	lemul12ad 10966	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ≤ (((abs‘𝑥) + 1) · 𝑇))
119	63, 70, 71, 74, 91, 118	le2addd 10646	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))) ≤ (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
120		eqid 2622	. . . . . . . . . . . . . 14 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
121	2, 120, 3, 9, 27	imsdval2 27542	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
122	31, 35, 43, 121	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
123		neg1cn 11124	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
124		mulcl 10020	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-1 · 𝑧) ∈ ℂ)
125	123, 36, 124	sylancr 695	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) ∈ ℂ)
126	2, 120, 3	nvdir 27486	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ ℂ ∧ (-1 · 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
127	31, 32, 125, 33, 126	syl13anc 1328	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
128	36	mulm1d 10482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) = -𝑧)
129	128	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 + -𝑧))
130	32, 36	negsubd 10398	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
131	129, 130	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 − 𝑧))
132	131	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥 − 𝑧)𝑆𝑦))
133	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → -1 ∈ ℂ)
134	2, 3	nvsass 27483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
135	31, 133, 36, 33, 134	syl13anc 1328	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
136	135	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
137	127, 132, 136	3eqtr3d 2664	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 − 𝑧)𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
138	137	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
139	2, 3, 9	nvs 27518	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 − 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
140	31, 61, 33, 139	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
141	122, 138, 140	3eqtr2d 2662	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
142	2, 65, 9, 27	imsdval 27541	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
143	31, 43, 39, 142	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
144	2, 65, 3	nvmdi 27503	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
145	31, 36, 33, 37, 144	syl13anc 1328	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
146	145	fveq2d 6195	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
147	2, 3, 9	nvs 27518	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
148	31, 36, 67, 147	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
149	143, 146, 148	3eqtr2d 2662	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
150	141, 149	oveq12d 6668	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) = (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))))
151	54	recnd 10068	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℂ)
152		1cnd 10056	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℂ)
153	89, 151, 152	addassd 10062	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) = ((𝑁‘𝑦) + ((abs‘𝑥) + 1)))
154	153	oveq1d 6665	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇))
155	73	recnd 10068	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℂ)
156	89, 155, 88	adddird 10065	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
157	154, 156	eqtrd 2656	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
158	119, 150, 157	3brtr4d 4685	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ≤ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇))
159	57	recnd 10068	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℂ)
160	105	rpcnd 11874	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℂ)
161	105	rpne0d 11877	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ≠ 0)
162	159, 160, 161	divrecd 10804	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))))
163	6	oveq2i 6661	. . . . . . . . . . 11 ⊢ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
164	162, 163	syl6reqr 2675	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
165		simplr 792	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ⁺)
166	102	rpred 11872	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ)
167	166	ltp1d 10954	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1))
168	102	rpcnd 11874	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℂ)
169	168, 152	addcomd 10238	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1) = (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
170	167, 169	breqtrd 4679	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
171	57, 165, 105, 170	ltdiv23d 11937	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 𝑟)
172	164, 171	eqbrtrd 4675	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) < 𝑟)
173	48, 60, 50, 158, 172	lelttrd 10195	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) < 𝑟)
174	41, 48, 50, 52, 173	lelttrd 10195	. . . . . . 7 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
175	174	expr 643	. . . . . 6 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋)) → (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
176	175	ralrimivva 2971	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
177		breq2 4657	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑥(abs ∘ − )𝑧) < 𝑠 ↔ (𝑥(abs ∘ − )𝑧) < 𝑇))
178		breq2 4657	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑦𝐶𝑤) < 𝑠 ↔ (𝑦𝐶𝑤) < 𝑇))
179	177, 178	anbi12d 747	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) ↔ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇)))
180	179	imbi1d 331	. . . . . . 7 ⊢ (𝑠 = 𝑇 → ((((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
181	180	2ralbidv 2989	. . . . . 6 ⊢ (𝑠 = 𝑇 → (∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
182	181	rspcev 3309	. . . . 5 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
183	26, 176, 182	syl2anc 693	. . . 4 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
184	183	ralrimiva 2966	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
185	184	rgen2 2975	. 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
186		cnxmet 22576	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
187	2, 27	imsxmet 27547	. . . 4 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
188	1, 187	ax-mp 5	. . 3 ⊢ 𝐶 ∈ (∞Met‘𝑋)
189		smcn.k	. . . . 5 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
190	189	cnfldtopn 22585	. . . 4 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
191		smcn.j	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
192	190, 191, 191	txmetcn 22353	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (∞Met‘𝑋)) → (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))))
193	186, 188, 188, 192	mp3an 1424	. 2 ⊢ (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
194	5, 185, 193	mpbir2an 955	1 ⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 class class class wbr 4653 × cxp 5112 ∘ ccom 5118 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℝ⁺crp 11832 abscabs 13974 TopOpenctopn 16082 ∞Metcxmt 19731 Metcme 19732 MetOpencmopn 19736 ℂ_fldccnfld 19746 Cn ccn 21028 ×_t ctx 21363 NrmCVeccnv 27439 +_𝑣 cpv 27440 BaseSetcba 27441 ·_𝑠OLD cns 27442 −_𝑣 cnsb 27444 norm_CVcnmcv 27445 IndMetcims 27446

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cn 21031 df-cnp 21032 df-tx 21365 df-hmeo 21558 df-xms 22125 df-tms 22127 df-grpo 27347 df-gid 27348 df-ginv 27349 df-gdiv 27350 df-ablo 27399 df-vc 27414 df-nv 27447 df-va 27450 df-ba 27451 df-sm 27452 df-0v 27453 df-vs 27454 df-nmcv 27455 df-ims 27456

This theorem is referenced by: smcn 27553

W3C validator