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 26936

Description: Lemma for smcn 26937. (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 26858	. . 3 ⊢ (𝑈 ∈ NrmCVec → 𝑆:(ℂ × 𝑋)⟶𝑋)
5	1, 4	ax-mp 5	. 2 ⊢ 𝑆:(ℂ × 𝑋)⟶𝑋
6		smcn.t	. . . . . 6 ⊢ 𝑇 = (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
7		1rp 11712	. . . . . . . 8 ⊢ 1 ∈ ℝ⁺
8		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
9		smcn.n	. . . . . . . . . . . . 13 ⊢ 𝑁 = (norm_CV‘𝑈)
10	2, 9	nvcl 26900	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
11	1, 8, 10	sylancr 694	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ)
12		abscl 13866	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (abs‘𝑥) ∈ ℝ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (abs‘𝑥) ∈ ℝ)
14	11, 13	readdcld 9948	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
15	2, 9	nvge0 26912	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
16	1, 8, 15	sylancr 694	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (𝑁‘𝑦))
17		absge0 13875	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → 0 ≤ (abs‘𝑥))
18	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ (abs‘𝑥))
19	11, 13, 16, 18	addge0d 10482	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → 0 ≤ ((𝑁‘𝑦) + (abs‘𝑥)))
20	14, 19	ge0p1rpd 11778	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺)
21		rpdivcl 11732	. . . . . . . . 9 ⊢ (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ⁺ ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
22	20, 21	sylan 487	. . . . . . . 8 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
23		rpaddcl 11730	. . . . . . . 8 ⊢ ((1 ∈ ℝ⁺ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
24	7, 22, 23	sylancr 694	. . . . . . 7 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
25	24	rpreccld 11758	. . . . . 6 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) ∈ ℝ⁺)
26	6, 25	syl5eqel 2692	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → 𝑇 ∈ ℝ⁺)
27		smcn.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (IndMet‘𝑈)
28	2, 27	imsmet 26930	. . . . . . . . . . 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 794	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑥 ∈ ℂ)
33		simpllr 795	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑦 ∈ 𝑋)
34	2, 3	nvscl 26865	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑥𝑆𝑦) ∈ 𝑋)
35	31, 32, 33, 34	syl3anc 1318	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥𝑆𝑦) ∈ 𝑋)
36		simprll 798	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑧 ∈ ℂ)
37		simprlr 799	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑤 ∈ 𝑋)
38	2, 3	nvscl 26865	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) → (𝑧𝑆𝑤) ∈ 𝑋)
39	31, 36, 37, 38	syl3anc 1318	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑤) ∈ 𝑋)
40		metcl 21947	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
41	30, 35, 39, 40	syl3anc 1318	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
42	2, 3	nvscl 26865	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑧𝑆𝑦) ∈ 𝑋)
43	31, 36, 33, 42	syl3anc 1318	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆𝑦) ∈ 𝑋)
44		metcl 21947	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
45	30, 35, 43, 44	syl3anc 1318	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) ∈ ℝ)
46		metcl 21947	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
47	30, 43, 39, 46	syl3anc 1318	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) ∈ ℝ)
48	45, 47	readdcld 9948	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ∈ ℝ)
49		rpre 11715	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
50	49	ad2antlr 759	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ)
51		mettri 21967	. . . . . . . . 9 ⊢ ((𝐶 ∈ (Met‘𝑋) ∧ ((𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋)) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
52	30, 35, 39, 43, 51	syl13anc 1320	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) ≤ (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))))
53	1, 33, 10	sylancr 694	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℝ)
54	32	abscld 14023	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℝ)
55	53, 54	readdcld 9948	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ)
56		peano2re 10088	. . . . . . . . . . 11 ⊢ (((𝑁‘𝑦) + (abs‘𝑥)) ∈ ℝ → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℝ)
58	26	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ⁺)
59	58	rpred 11748	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℝ)
60	57, 59	remulcld 9949	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) ∈ ℝ)
61	32, 36	subcld 10271	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 − 𝑧) ∈ ℂ)
62	61	abscld 14023	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ∈ ℝ)
63	62, 53	remulcld 9949	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ∈ ℝ)
64	36	abscld 14023	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ∈ ℝ)
65		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ ( −_𝑣 ‘𝑈) = ( −_𝑣 ‘𝑈)
66	2, 65	nvmcl 26885	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
67	31, 33, 37, 66	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋)
68	2, 9	nvcl 26900	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
69	1, 67, 68	sylancr 694	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ∈ ℝ)
70	64, 69	remulcld 9949	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ∈ ℝ)
71	53, 59	remulcld 9949	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑁‘𝑦) · 𝑇) ∈ ℝ)
72		peano2re 10088	. . . . . . . . . . . . 13 ⊢ ((abs‘𝑥) ∈ ℝ → ((abs‘𝑥) + 1) ∈ ℝ)
73	54, 72	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℝ)
74	73, 59	remulcld 9949	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘𝑥) + 1) · 𝑇) ∈ ℝ)
75	1, 33, 15	sylancr 694	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘𝑦))
76	32, 36	abssubd 14040	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) = (abs‘(𝑧 − 𝑥)))
77	36, 32	subcld 10271	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧 − 𝑥) ∈ ℂ)
78	77	abscld 14023	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ∈ ℝ)
79		eqid 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
80	79	cnmetdval 22384	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
81	32, 36, 80	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧)))
82	81, 76	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑧 − 𝑥)))
83		simprrl 800	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥(abs ∘ − )𝑧) < 𝑇)
84	82, 83	eqbrtrrd 4607	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) < 𝑇)
85	78, 59, 84	ltled 10064	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 𝑇)
86	76, 85	eqbrtrd 4605	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 − 𝑧)) ≤ 𝑇)
87	62, 59, 53, 75, 86	lemul1ad 10842	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ (𝑇 · (𝑁‘𝑦)))
88	58	rpcnd 11750	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ∈ ℂ)
89	53	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘𝑦) ∈ ℂ)
90	88, 89	mulcomd 9940	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑇 · (𝑁‘𝑦)) = ((𝑁‘𝑦) · 𝑇))
91	87, 90	breqtrd 4609	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) ≤ ((𝑁‘𝑦) · 𝑇))
92	36	absge0d 14031	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (abs‘𝑧))
93	2, 9	nvge0 26912	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
94	1, 67, 93	sylancr 694	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 0 ≤ (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
95	54, 78	readdcld 9948	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ∈ ℝ)
96	32, 36	pncan3d 10274	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (𝑧 − 𝑥)) = 𝑧)
97	96	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) = (abs‘𝑧))
98	32, 77	abstrid 14043	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑥 + (𝑧 − 𝑥))) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
99	97, 98	eqbrtrrd 4607	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))))
100		1red 9934	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℝ)
101		1re 9918	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
102	22	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺)
103		ltaddrp 11743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ⁺) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
104	101, 102, 103	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
105	24	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℝ⁺)
106	105	recgt1d 11762	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ↔ (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1))
107	104, 106	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 1)
108	6, 107	syl5eqbr 4618	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 < 1)
109	59, 100, 108	ltled 10064	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑇 ≤ 1)
110	78, 59, 100, 85, 109	letrd 10073	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘(𝑧 − 𝑥)) ≤ 1)
111	78, 100, 54, 110	leadd2dd 10521	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + (abs‘(𝑧 − 𝑥))) ≤ ((abs‘𝑥) + 1))
112	64, 95, 73, 99, 111	letrd 10073	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑧) ≤ ((abs‘𝑥) + 1))
113	2, 65, 9, 27	imsdval 26925	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
114	31, 33, 37, 113	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) = (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))
115		simprrr 801	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑦𝐶𝑤) < 𝑇)
116	114, 115	eqbrtrrd 4607	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) < 𝑇)
117	69, 59, 116	ltled 10064	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)) ≤ 𝑇)
118	64, 73, 69, 59, 92, 94, 112, 117	lemul12ad 10845	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))) ≤ (((abs‘𝑥) + 1) · 𝑇))
119	63, 70, 71, 74, 91, 118	le2addd 10525	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))) ≤ (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
120		eqid 2610	. . . . . . . . . . . . . 14 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
121	2, 120, 3, 9, 27	imsdval2 26926	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑦) ∈ 𝑋) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
122	31, 35, 43, 121	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
123		neg1cn 11001	. . . . . . . . . . . . . . . 16 ⊢ -1 ∈ ℂ
124		mulcl 9899	. . . . . . . . . . . . . . . 16 ⊢ ((-1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (-1 · 𝑧) ∈ ℂ)
125	123, 36, 124	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) ∈ ℂ)
126	2, 120, 3	nvdir 26870	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ ℂ ∧ (-1 · 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
127	31, 32, 125, 33, 126	syl13anc 1320	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)))
128	36	mulm1d 10361	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (-1 · 𝑧) = -𝑧)
129	128	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 + -𝑧))
130	32, 36	negsubd 10277	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + -𝑧) = (𝑥 − 𝑧))
131	129, 130	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑥 + (-1 · 𝑧)) = (𝑥 − 𝑧))
132	131	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 + (-1 · 𝑧))𝑆𝑦) = ((𝑥 − 𝑧)𝑆𝑦))
133	123	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → -1 ∈ ℂ)
134	2, 3	nvsass 26867	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋)) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
135	31, 133, 36, 33, 134	syl13anc 1320	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((-1 · 𝑧)𝑆𝑦) = (-1𝑆(𝑧𝑆𝑦)))
136	135	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)((-1 · 𝑧)𝑆𝑦)) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
137	127, 132, 136	3eqtr3d 2652	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥 − 𝑧)𝑆𝑦) = ((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦))))
138	137	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = (𝑁‘((𝑥𝑆𝑦)( +_𝑣 ‘𝑈)(-1𝑆(𝑧𝑆𝑦)))))
139	2, 3, 9	nvs 26902	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 − 𝑧) ∈ ℂ ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
140	31, 61, 33, 139	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘((𝑥 − 𝑧)𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
141	122, 138, 140	3eqtr2d 2650	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) = ((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)))
142	2, 65, 9, 27	imsdval 26925	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧𝑆𝑦) ∈ 𝑋 ∧ (𝑧𝑆𝑤) ∈ 𝑋) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
143	31, 43, 39, 142	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
144	2, 65, 3	nvmdi 26887	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑧 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
145	31, 36, 33, 37, 144	syl13anc 1320	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤)) = ((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤)))
146	145	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = (𝑁‘((𝑧𝑆𝑦)( −_𝑣 ‘𝑈)(𝑧𝑆𝑤))))
147	2, 3, 9	nvs 26902	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ ℂ ∧ (𝑦( −_𝑣 ‘𝑈)𝑤) ∈ 𝑋) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
148	31, 36, 67, 147	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (𝑁‘(𝑧𝑆(𝑦( −_𝑣 ‘𝑈)𝑤))) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
149	143, 146, 148	3eqtr2d 2650	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤)) = ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤))))
150	141, 149	oveq12d 6567	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) = (((abs‘(𝑥 − 𝑧)) · (𝑁‘𝑦)) + ((abs‘𝑧) · (𝑁‘(𝑦( −_𝑣 ‘𝑈)𝑤)))))
151	54	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (abs‘𝑥) ∈ ℂ)
152		1cnd 9935	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 1 ∈ ℂ)
153	89, 151, 152	addassd 9941	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) = ((𝑁‘𝑦) + ((abs‘𝑥) + 1)))
154	153	oveq1d 6564	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇))
155	73	recnd 9947	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((abs‘𝑥) + 1) ∈ ℂ)
156	89, 155, 88	adddird 9944	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + ((abs‘𝑥) + 1)) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
157	154, 156	eqtrd 2644	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = (((𝑁‘𝑦) · 𝑇) + (((abs‘𝑥) + 1) · 𝑇)))
158	119, 150, 157	3brtr4d 4615	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) ≤ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇))
159	57	recnd 9947	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑁‘𝑦) + (abs‘𝑥)) + 1) ∈ ℂ)
160	105	rpcnd 11750	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ∈ ℂ)
161	105	rpne0d 11753	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)) ≠ 0)
162	159, 160, 161	divrecd 10683	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))))
163	6	oveq2i 6560	. . . . . . . . . . 11 ⊢ ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · (1 / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
164	162, 163	syl6reqr 2663	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) = ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))))
165		simplr 788	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → 𝑟 ∈ ℝ⁺)
166	102	rpred 11748	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℝ)
167	166	ltp1d 10833	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1))
168	102	rpcnd 11750	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) ∈ ℂ)
169	168, 152	addcomd 10117	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) + 1) = (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
170	167, 169	breqtrd 4609	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟) < (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟)))
171	57, 165, 105, 170	ltdiv23d 11813	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / (1 + ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) / 𝑟))) < 𝑟)
172	164, 171	eqbrtrd 4605	. . . . . . . . 9 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((((𝑁‘𝑦) + (abs‘𝑥)) + 1) · 𝑇) < 𝑟)
173	48, 60, 50, 158, 172	lelttrd 10074	. . . . . . . 8 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → (((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑦)) + ((𝑧𝑆𝑦)𝐶(𝑧𝑆𝑤))) < 𝑟)
174	41, 48, 50, 52, 173	lelttrd 10074	. . . . . . 7 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ ((𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋) ∧ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇))) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
175	174	expr 641	. . . . . 6 ⊢ ((((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑧 ∈ ℂ ∧ 𝑤 ∈ 𝑋)) → (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
176	175	ralrimivva 2954	. . . . 5 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
177		breq2 4587	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑥(abs ∘ − )𝑧) < 𝑠 ↔ (𝑥(abs ∘ − )𝑧) < 𝑇))
178		breq2 4587	. . . . . . . . 9 ⊢ (𝑠 = 𝑇 → ((𝑦𝐶𝑤) < 𝑠 ↔ (𝑦𝐶𝑤) < 𝑇))
179	177, 178	anbi12d 743	. . . . . . . 8 ⊢ (𝑠 = 𝑇 → (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) ↔ ((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇)))
180	179	imbi1d 330	. . . . . . 7 ⊢ (𝑠 = 𝑇 → ((((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
181	180	2ralbidv 2972	. . . . . 6 ⊢ (𝑠 = 𝑇 → (∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
182	181	rspcev 3282	. . . . 5 ⊢ ((𝑇 ∈ ℝ⁺ ∧ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑇 ∧ (𝑦𝐶𝑤) < 𝑇) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
183	26, 176, 182	syl2anc 691	. . . 4 ⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
184	183	ralrimiva 2949	. . 3 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝑋) → ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))
185	184	rgen2 2958	. 2 ⊢ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)
186		cnxmet 22386	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
187	2, 27	imsxmet 26931	. . . 4 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋))
188	1, 187	ax-mp 5	. . 3 ⊢ 𝐶 ∈ (∞Met‘𝑋)
189		smcn.k	. . . . 5 ⊢ 𝐾 = (TopOpen‘ℂ_fld)
190	189	cnfldtopn 22395	. . . 4 ⊢ 𝐾 = (MetOpen‘(abs ∘ − ))
191		smcn.j	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
192	190, 191, 191	txmetcn 22163	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (∞Met‘𝑋)) → (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟))))
193	186, 188, 188, 192	mp3an 1416	. 2 ⊢ (𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽) ↔ (𝑆:(ℂ × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ ∀𝑧 ∈ ℂ ∀𝑤 ∈ 𝑋 (((𝑥(abs ∘ − )𝑧) < 𝑠 ∧ (𝑦𝐶𝑤) < 𝑠) → ((𝑥𝑆𝑦)𝐶(𝑧𝑆𝑤)) < 𝑟)))
194	5, 185, 193	mpbir2an 957	1 ⊢ 𝑆 ∈ ((𝐾 ×_t 𝐽) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 class class class wbr 4583 × cxp 5036 ∘ ccom 5042 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℝ⁺crp 11708 abscabs 13822 TopOpenctopn 15905 ∞Metcxmt 19552 Metcme 19553 MetOpencmopn 19557 ℂ_fldccnfld 19567 Cn ccn 20838 ×_t ctx 21173 NrmCVeccnv 26823 +_𝑣 cpv 26824 BaseSetcba 26825 ·_𝑠OLD cns 26826 −_𝑣 cnsb 26828 norm_CVcnmcv 26829 IndMetcims 26830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894 ax-mulf 9895

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-supp 7183 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fsupp 8159 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-icc 12053 df-fz 12198 df-fzo 12335 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-sets 15701 df-ress 15702 df-plusg 15781 df-mulr 15782 df-starv 15783 df-sca 15784 df-vsca 15785 df-ip 15786 df-tset 15787 df-ple 15788 df-ds 15791 df-unif 15792 df-hom 15793 df-cco 15794 df-rest 15906 df-topn 15907 df-0g 15925 df-gsum 15926 df-topgen 15927 df-pt 15928 df-prds 15931 df-xrs 15985 df-qtop 15990 df-imas 15991 df-xps 15993 df-mre 16069 df-mrc 16070 df-acs 16072 df-mgm 17065 df-sgrp 17107 df-mnd 17118 df-submnd 17159 df-mulg 17364 df-cntz 17573 df-cmn 18018 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-cnfld 19568 df-top 20521 df-bases 20522 df-topon 20523 df-topsp 20524 df-cn 20841 df-cnp 20842 df-tx 21175 df-hmeo 21368 df-xms 21935 df-tms 21937 df-grpo 26731 df-gid 26732 df-ginv 26733 df-gdiv 26734 df-ablo 26783 df-vc 26798 df-nv 26831 df-va 26834 df-ba 26835 df-sm 26836 df-0v 26837 df-vs 26838 df-nmcv 26839 df-ims 26840

This theorem is referenced by: smcn 26937

W3C validator