blocnilem

Description: Lemma for blocni and lnocni . If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007) (Revised by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	blocni.8	$⊢ C = IndMet (U)$
	blocni.d	$⊢ D = IndMet (W)$
	blocni.j	$⊢ J = MetOpen (C)$
	blocni.k	$⊢ K = MetOpen (D)$
	blocni.4	$⊢ L = U LnOp W$
	blocni.5	$⊢ B = U BLnOp W$
	blocni.u	$⊢ U \in NrmCVec$
	blocni.w	$⊢ W \in NrmCVec$
	blocni.l	$⊢ T \in L$
	blocnilem.1	$⊢ X = BaseSet (U)$
Assertion	blocnilem	$⊢ (P \in X \land T \in (J CnP K) (P)) \to T \in B$

Proof

Step	Hyp	Ref	Expression
1		blocni.8	$⊢ C = IndMet (U)$
2		blocni.d	$⊢ D = IndMet (W)$
3		blocni.j	$⊢ J = MetOpen (C)$
4		blocni.k	$⊢ K = MetOpen (D)$
5		blocni.4	$⊢ L = U LnOp W$
6		blocni.5	$⊢ B = U BLnOp W$
7		blocni.u	$⊢ U \in NrmCVec$
8		blocni.w	$⊢ W \in NrmCVec$
9		blocni.l	$⊢ T \in L$
10		blocnilem.1	$⊢ X = BaseSet (U)$
11	10 1	imsxmet	$⊢ U \in NrmCVec \to C \in ∞Met (X)$
12	7 11	ax-mp	$⊢ C \in ∞Met (X)$
13		eqid	$⊢ BaseSet (W) = BaseSet (W)$
14	13 2	imsxmet	$⊢ W \in NrmCVec \to D \in ∞Met (BaseSet (W))$
15	8 14	ax-mp	$⊢ D \in ∞Met (BaseSet (W))$
16		1rp	$⊢ 1 \in ℝ^{+}$
17	3 4	metcnpi3	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (BaseSet (W))) \land (T \in (J CnP K) (P) \land 1 \in ℝ^{+})) \to \exists y \in ℝ^{+} \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)$
18	16 17	mpanr2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (BaseSet (W))) \land T \in (J CnP K) (P)) \to \exists y \in ℝ^{+} \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)$
19	12 15 18	mpanl12	$⊢ T \in (J CnP K) (P) \to \exists y \in ℝ^{+} \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)$
20		rpreccl	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℝ^{+}$
21	20	rpred	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℝ$
22	21	ad2antlr	$⊢ ((P \in X \land y \in ℝ^{+}) \land \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)) \to \frac{1}{y} \in ℝ$
23		eqid	$⊢ -_{v} (U) = -_{v} (U)$
24		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
25	10 23 24 1	imsdval	$⊢ (U \in NrmCVec \land x \in X \land P \in X) \to x C P = {norm}_{CV} (U) (x -_{v} (U) P)$
26	7 25	mp3an1	$⊢ (x \in X \land P \in X) \to x C P = {norm}_{CV} (U) (x -_{v} (U) P)$
27	26	breq1d	$⊢ (x \in X \land P \in X) \to (x C P \leq y \leftrightarrow {norm}_{CV} (U) (x -_{v} (U) P) \leq y)$
28	10 13 5	lnof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T : X ⟶ BaseSet (W)$
29	7 8 9 28	mp3an	$⊢ T : X ⟶ BaseSet (W)$
30	29	ffvelcdmi	$⊢ x \in X \to T (x) \in BaseSet (W)$
31	29	ffvelcdmi	$⊢ P \in X \to T (P) \in BaseSet (W)$
32		eqid	$⊢ -_{v} (W) = -_{v} (W)$
33		eqid	$⊢ {norm}_{CV} (W) = {norm}_{CV} (W)$
34	13 32 33 2	imsdval	$⊢ (W \in NrmCVec \land T (x) \in BaseSet (W) \land T (P) \in BaseSet (W)) \to T (x) D T (P) = {norm}_{CV} (W) (T (x) -_{v} (W) T (P))$
35	8 34	mp3an1	$⊢ (T (x) \in BaseSet (W) \land T (P) \in BaseSet (W)) \to T (x) D T (P) = {norm}_{CV} (W) (T (x) -_{v} (W) T (P))$
36	30 31 35	syl2an	$⊢ (x \in X \land P \in X) \to T (x) D T (P) = {norm}_{CV} (W) (T (x) -_{v} (W) T (P))$
37	7 8 9	3pm3.2i	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L)$
38	10 23 32 5	lnosub	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (x \in X \land P \in X)) \to T (x -_{v} (U) P) = T (x) -_{v} (W) T (P)$
39	37 38	mpan	$⊢ (x \in X \land P \in X) \to T (x -_{v} (U) P) = T (x) -_{v} (W) T (P)$
40	39	fveq2d	$⊢ (x \in X \land P \in X) \to {norm}_{CV} (W) (T (x -_{v} (U) P)) = {norm}_{CV} (W) (T (x) -_{v} (W) T (P))$
41	36 40	eqtr4d	$⊢ (x \in X \land P \in X) \to T (x) D T (P) = {norm}_{CV} (W) (T (x -_{v} (U) P))$
42	41	breq1d	$⊢ (x \in X \land P \in X) \to (T (x) D T (P) \leq 1 \leftrightarrow {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1)$
43	27 42	imbi12d	$⊢ (x \in X \land P \in X) \to ((x C P \leq y \to T (x) D T (P) \leq 1) \leftrightarrow ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1))$
44	43	ancoms	$⊢ (P \in X \land x \in X) \to ((x C P \leq y \to T (x) D T (P) \leq 1) \leftrightarrow ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1))$
45	44	adantlr	$⊢ ((P \in X \land y \in ℝ^{+}) \land x \in X) \to ((x C P \leq y \to T (x) D T (P) \leq 1) \leftrightarrow ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1))$
46	45	ralbidva	$⊢ (P \in X \land y \in ℝ^{+}) \to (\forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1) \leftrightarrow \forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1))$
47		2fveq3	$⊢ z = 0_{vec} (U) \to {norm}_{CV} (W) (T (z)) = {norm}_{CV} (W) (T (0_{vec} (U)))$
48		fveq2	$⊢ z = 0_{vec} (U) \to {norm}_{CV} (U) (z) = {norm}_{CV} (U) (0_{vec} (U))$
49	48	oveq2d	$⊢ z = 0_{vec} (U) \to (\frac{1}{y}) {norm}_{CV} (U) (z) = (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U))$
50	47 49	breq12d	$⊢ z = 0_{vec} (U) \to ({norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z) \leftrightarrow {norm}_{CV} (W) (T (0_{vec} (U))) \leq (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U)))$
51	7	a1i	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to U \in NrmCVec$
52		simpll	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to P \in X$
53		simpr	$⊢ (P \in X \land y \in ℝ^{+}) \to y \in ℝ^{+}$
54	10 24	nvcl	$⊢ (U \in NrmCVec \land z \in X) \to {norm}_{CV} (U) (z) \in ℝ$
55	7 54	mpan	$⊢ z \in X \to {norm}_{CV} (U) (z) \in ℝ$
56	55	adantr	$⊢ (z \in X \land z \neq 0_{vec} (U)) \to {norm}_{CV} (U) (z) \in ℝ$
57		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
58	10 57 24	nvgt0	$⊢ (U \in NrmCVec \land z \in X) \to (z \neq 0_{vec} (U) \leftrightarrow 0 < {norm}_{CV} (U) (z))$
59	7 58	mpan	$⊢ z \in X \to (z \neq 0_{vec} (U) \leftrightarrow 0 < {norm}_{CV} (U) (z))$
60	59	biimpa	$⊢ (z \in X \land z \neq 0_{vec} (U)) \to 0 < {norm}_{CV} (U) (z)$
61	56 60	elrpd	$⊢ (z \in X \land z \neq 0_{vec} (U)) \to {norm}_{CV} (U) (z) \in ℝ^{+}$
62		rpdivcl	$⊢ (y \in ℝ^{+} \land {norm}_{CV} (U) (z) \in ℝ^{+}) \to \frac{y}{{norm}_{CV} (U) (z)} \in ℝ^{+}$
63	53 61 62	syl2an	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to \frac{y}{{norm}_{CV} (U) (z)} \in ℝ^{+}$
64	63	rpcnd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to \frac{y}{{norm}_{CV} (U) (z)} \in ℂ$
65		simprl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to z \in X$
66		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
67	10 66	nvscl	$⊢ (U \in NrmCVec \land \frac{y}{{norm}_{CV} (U) (z)} \in ℂ \land z \in X) \to (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z \in X$
68	51 64 65 67	syl3anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z \in X$
69		eqid	$⊢ +_{v} (U) = +_{v} (U)$
70	10 69 23	nvpncan2	$⊢ (U \in NrmCVec \land P \in X \land (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z \in X) \to (P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z$
71	51 52 68 70	syl3anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z$
72	71	fveq2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) = {norm}_{CV} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)$
73	63	rprege0d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\frac{y}{{norm}_{CV} (U) (z)} \in ℝ \land 0 \leq \frac{y}{{norm}_{CV} (U) (z)})$
74	10 66 24	nvsge0	$⊢ (U \in NrmCVec \land (\frac{y}{{norm}_{CV} (U) (z)} \in ℝ \land 0 \leq \frac{y}{{norm}_{CV} (U) (z)}) \land z \in X) \to {norm}_{CV} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) = (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (U) (z)$
75	51 73 65 74	syl3anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) = (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (U) (z)$
76		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
77	76	ad2antlr	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to y \in ℂ$
78	55	ad2antrl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) (z) \in ℝ$
79	78	recnd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) (z) \in ℂ$
80	10 57 24	nvz	$⊢ (U \in NrmCVec \land z \in X) \to ({norm}_{CV} (U) (z) = 0 \leftrightarrow z = 0_{vec} (U))$
81	7 80	mpan	$⊢ z \in X \to ({norm}_{CV} (U) (z) = 0 \leftrightarrow z = 0_{vec} (U))$
82	81	necon3bid	$⊢ z \in X \to ({norm}_{CV} (U) (z) \neq 0 \leftrightarrow z \neq 0_{vec} (U))$
83	82	biimpar	$⊢ (z \in X \land z \neq 0_{vec} (U)) \to {norm}_{CV} (U) (z) \neq 0$
84	83	adantl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) (z) \neq 0$
85	77 79 84	divcan1d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (U) (z) = y$
86	72 75 85	3eqtrd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) = y$
87		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
88	87	leidd	$⊢ y \in ℝ^{+} \to y \leq y$
89	88	ad2antlr	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to y \leq y$
90	86 89	eqbrtrd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) \leq y$
91	10 69	nvgcl	$⊢ (U \in NrmCVec \land P \in X \land (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z \in X) \to P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \in X$
92	51 52 68 91	syl3anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \in X$
93		fvoveq1	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to {norm}_{CV} (U) (x -_{v} (U) P) = {norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)$
94	93	breq1d	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \leftrightarrow {norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) \leq y)$
95		fvoveq1	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to T (x -_{v} (U) P) = T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)$
96	95	fveq2d	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to {norm}_{CV} (W) (T (x -_{v} (U) P)) = {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P))$
97	96	breq1d	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to ({norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1 \leftrightarrow {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1)$
98	94 97	imbi12d	$⊢ x = P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \to (({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \leftrightarrow ({norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1))$
99	98	rspcv	$⊢ P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) \in X \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to ({norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1))$
100	92 99	syl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to ({norm}_{CV} (U) ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1))$
101	90 100	mpid	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1)$
102	29	ffvelcdmi	$⊢ z \in X \to T (z) \in BaseSet (W)$
103	13 33	nvcl	$⊢ (W \in NrmCVec \land T (z) \in BaseSet (W)) \to {norm}_{CV} (W) (T (z)) \in ℝ$
104	8 102 103	sylancr	$⊢ z \in X \to {norm}_{CV} (W) (T (z)) \in ℝ$
105	104	ad2antrl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (W) (T (z)) \in ℝ$
106		1red	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to 1 \in ℝ$
107	105 106 63	lemuldiv2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to ((\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (W) (T (z)) \leq 1 \leftrightarrow {norm}_{CV} (W) (T (z)) \leq \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}})$
108	71	fveq2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) = T ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)$
109		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
110	10 66 109 5	lnomul	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land (\frac{y}{{norm}_{CV} (U) (z)} \in ℂ \land z \in X)) \to T ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)$
111	37 110	mpan	$⊢ (\frac{y}{{norm}_{CV} (U) (z)} \in ℂ \land z \in X) \to T ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)$
112	64 65 111	syl2anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to T ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z) = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)$
113	108 112	eqtrd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P) = (\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)$
114	113	fveq2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) = {norm}_{CV} (W) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z))$
115	8	a1i	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to W \in NrmCVec$
116	102	ad2antrl	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to T (z) \in BaseSet (W)$
117	13 109 33	nvsge0	$⊢ (W \in NrmCVec \land (\frac{y}{{norm}_{CV} (U) (z)} \in ℝ \land 0 \leq \frac{y}{{norm}_{CV} (U) (z)}) \land T (z) \in BaseSet (W)) \to {norm}_{CV} (W) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)) = (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (W) (T (z))$
118	115 73 116 117	syl3anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (W) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (W) T (z)) = (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (W) (T (z))$
119	114 118	eqtrd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to {norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) = (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (W) (T (z))$
120	119	breq1d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to ({norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1 \leftrightarrow (\frac{y}{{norm}_{CV} (U) (z)}) {norm}_{CV} (W) (T (z)) \leq 1)$
121		rpcnne0	$⊢ y \in ℝ^{+} \to (y \in ℂ \land y \neq 0)$
122		rpcnne0	$⊢ {norm}_{CV} (U) (z) \in ℝ^{+} \to ({norm}_{CV} (U) (z) \in ℂ \land {norm}_{CV} (U) (z) \neq 0)$
123		recdiv	$⊢ ((y \in ℂ \land y \neq 0) \land ({norm}_{CV} (U) (z) \in ℂ \land {norm}_{CV} (U) (z) \neq 0)) \to \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}} = \frac{{norm}_{CV} (U) (z)}{y}$
124	121 122 123	syl2an	$⊢ (y \in ℝ^{+} \land {norm}_{CV} (U) (z) \in ℝ^{+}) \to \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}} = \frac{{norm}_{CV} (U) (z)}{y}$
125	53 61 124	syl2an	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}} = \frac{{norm}_{CV} (U) (z)}{y}$
126		rpne0	$⊢ y \in ℝ^{+} \to y \neq 0$
127	126	ad2antlr	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to y \neq 0$
128	79 77 127	divrec2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to \frac{{norm}_{CV} (U) (z)}{y} = (\frac{1}{y}) {norm}_{CV} (U) (z)$
129	125 128	eqtr2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\frac{1}{y}) {norm}_{CV} (U) (z) = \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}}$
130	129	breq2d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to ({norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z) \leftrightarrow {norm}_{CV} (W) (T (z)) \leq \frac{1}{\frac{y}{{norm}_{CV} (U) (z)}})$
131	107 120 130	3bitr4d	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to ({norm}_{CV} (W) (T ((P +_{v} (U) ((\frac{y}{{norm}_{CV} (U) (z)}) \cdot_{𝑠OLD} (U) z)) -_{v} (U) P)) \leq 1 \leftrightarrow {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
132	101 131	sylibd	$⊢ ((P \in X \land y \in ℝ^{+}) \land (z \in X \land z \neq 0_{vec} (U))) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
133	132	anassrs	$⊢ (((P \in X \land y \in ℝ^{+}) \land z \in X) \land z \neq 0_{vec} (U)) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
134	133	imp	$⊢ ((((P \in X \land y \in ℝ^{+}) \land z \in X) \land z \neq 0_{vec} (U)) \land \forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1)) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z)$
135	134	an32s	$⊢ ((((P \in X \land y \in ℝ^{+}) \land z \in X) \land \forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1)) \land z \neq 0_{vec} (U)) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z)$
136		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
137	10 13 57 136 5	lno0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T (0_{vec} (U)) = 0_{vec} (W)$
138	7 8 9 137	mp3an	$⊢ T (0_{vec} (U)) = 0_{vec} (W)$
139	138	fveq2i	$⊢ {norm}_{CV} (W) (T (0_{vec} (U))) = {norm}_{CV} (W) (0_{vec} (W))$
140	136 33	nvz0	$⊢ W \in NrmCVec \to {norm}_{CV} (W) (0_{vec} (W)) = 0$
141	8 140	ax-mp	$⊢ {norm}_{CV} (W) (0_{vec} (W)) = 0$
142	139 141	eqtri	$⊢ {norm}_{CV} (W) (T (0_{vec} (U))) = 0$
143		0le0	$⊢ 0 \leq 0$
144	142 143	eqbrtri	$⊢ {norm}_{CV} (W) (T (0_{vec} (U))) \leq 0$
145	20	rpcnd	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℂ$
146	57 24	nvz0	$⊢ U \in NrmCVec \to {norm}_{CV} (U) (0_{vec} (U)) = 0$
147	7 146	ax-mp	$⊢ {norm}_{CV} (U) (0_{vec} (U)) = 0$
148	147	oveq2i	$⊢ (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U)) = (\frac{1}{y}) \cdot 0$
149		mul01	$⊢ \frac{1}{y} \in ℂ \to (\frac{1}{y}) \cdot 0 = 0$
150	148 149	eqtrid	$⊢ \frac{1}{y} \in ℂ \to (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U)) = 0$
151	145 150	syl	$⊢ y \in ℝ^{+} \to (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U)) = 0$
152	144 151	breqtrrid	$⊢ y \in ℝ^{+} \to {norm}_{CV} (W) (T (0_{vec} (U))) \leq (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U))$
153	152	ad3antlr	$⊢ (((P \in X \land y \in ℝ^{+}) \land z \in X) \land \forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1)) \to {norm}_{CV} (W) (T (0_{vec} (U))) \leq (\frac{1}{y}) {norm}_{CV} (U) (0_{vec} (U))$
154	50 135 153	pm2.61ne	$⊢ (((P \in X \land y \in ℝ^{+}) \land z \in X) \land \forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1)) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z)$
155	154	ex	$⊢ ((P \in X \land y \in ℝ^{+}) \land z \in X) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
156	155	ralrimdva	$⊢ (P \in X \land y \in ℝ^{+}) \to (\forall x \in X ({norm}_{CV} (U) (x -_{v} (U) P) \leq y \to {norm}_{CV} (W) (T (x -_{v} (U) P)) \leq 1) \to \forall z \in X {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
157	46 156	sylbid	$⊢ (P \in X \land y \in ℝ^{+}) \to (\forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1) \to \forall z \in X {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
158	157	imp	$⊢ ((P \in X \land y \in ℝ^{+}) \land \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)) \to \forall z \in X {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z)$
159		oveq1	$⊢ x = \frac{1}{y} \to x {norm}_{CV} (U) (z) = (\frac{1}{y}) {norm}_{CV} (U) (z)$
160	159	breq2d	$⊢ x = \frac{1}{y} \to ({norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z) \leftrightarrow {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
161	160	ralbidv	$⊢ x = \frac{1}{y} \to (\forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z) \leftrightarrow \forall z \in X {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z))$
162	161	rspcev	$⊢ (\frac{1}{y} \in ℝ \land \forall z \in X {norm}_{CV} (W) (T (z)) \leq (\frac{1}{y}) {norm}_{CV} (U) (z)) \to \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z)$
163	22 158 162	syl2anc	$⊢ ((P \in X \land y \in ℝ^{+}) \land \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1)) \to \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z)$
164	163	rexlimdva2	$⊢ P \in X \to (\exists y \in ℝ^{+} \forall x \in X (x C P \leq y \to T (x) D T (P) \leq 1) \to \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z))$
165	19 164	syl5	$⊢ P \in X \to (T \in (J CnP K) (P) \to \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z))$
166	165	imp	$⊢ (P \in X \land T \in (J CnP K) (P)) \to \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z)$
167	10 24 33 5 6 7 8	isblo3i	$⊢ T \in B \leftrightarrow (T \in L \land \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z))$
168	9 167	mpbiran	$⊢ T \in B \leftrightarrow \exists x \in ℝ \forall z \in X {norm}_{CV} (W) (T (z)) \leq x {norm}_{CV} (U) (z)$
169	166 168	sylibr	$⊢ (P \in X \land T \in (J CnP K) (P)) \to T \in B$

Metamath Proof Explorer

Theorem blocnilem

Proof