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	$⊢ C = IndMet (U)$
	smcn.j	$⊢ J = MetOpen (C)$
	smcn.s	$⊢ S = \cdot_{𝑠OLD} (U)$
	smcn.k	$⊢ K = TopOpen (ℂ_{fld})$
	smcn.x	$⊢ X = BaseSet (U)$
	smcn.n	$⊢ N = {norm}_{CV} (U)$
	smcn.u	$⊢ U \in NrmCVec$
	smcn.t	$⊢ T = \frac{1}{1 + (\frac{N (y) + \|x\| + 1}{r})}$
Assertion	smcnlem	$⊢ S \in ((K \times_{t} J) Cn J)$

Proof

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

Metamath Proof Explorer

Theorem smcnlem

Proof