ubthlem2

Description: Lemma for ubth . Given that there is a closed ball B ( P , R ) in AK , for any x e. B ( 0 , 1 ) , we have P + R x. x e. B ( P , R ) and P e. B ( P , R ) , so both of these have norm ( t ( z ) ) <_ K and so norm ( t ( x ) ) <_ ( norm ( t ( P ) ) + norm ( t ( P + R x. x ) ) ) / R <_ ( K + K ) / R , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ubth.1	$⊢ X = BaseSet (U)$
	ubth.2	$⊢ N = {norm}_{CV} (W)$
	ubthlem.3	$⊢ D = IndMet (U)$
	ubthlem.4	$⊢ J = MetOpen (D)$
	ubthlem.5	$⊢ U \in CBan$
	ubthlem.6	$⊢ W \in NrmCVec$
	ubthlem.7	$⊢ φ \to T \subseteq U BLnOp W$
	ubthlem.8	$⊢ φ \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
	ubthlem.9	$⊢ A = (k \in ℕ ⟼ \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
	ubthlem.10	$⊢ φ \to K \in ℕ$
	ubthlem.11	$⊢ φ \to P \in X$
	ubthlem.12	$⊢ φ \to R \in ℝ^{+}$
	ubthlem.13	$⊢ φ \to \{z \in X \| P D z \leq R\} \subseteq A (K)$
Assertion	ubthlem2	$⊢ φ \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d$

Proof

Step	Hyp	Ref	Expression
1		ubth.1	$⊢ X = BaseSet (U)$
2		ubth.2	$⊢ N = {norm}_{CV} (W)$
3		ubthlem.3	$⊢ D = IndMet (U)$
4		ubthlem.4	$⊢ J = MetOpen (D)$
5		ubthlem.5	$⊢ U \in CBan$
6		ubthlem.6	$⊢ W \in NrmCVec$
7		ubthlem.7	$⊢ φ \to T \subseteq U BLnOp W$
8		ubthlem.8	$⊢ φ \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
9		ubthlem.9	$⊢ A = (k \in ℕ ⟼ \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
10		ubthlem.10	$⊢ φ \to K \in ℕ$
11		ubthlem.11	$⊢ φ \to P \in X$
12		ubthlem.12	$⊢ φ \to R \in ℝ^{+}$
13		ubthlem.13	$⊢ φ \to \{z \in X \| P D z \leq R\} \subseteq A (K)$
14	10	nnrpd	$⊢ φ \to K \in ℝ^{+}$
15	14 14	rpaddcld	$⊢ φ \to K + K \in ℝ^{+}$
16	15 12	rpdivcld	$⊢ φ \to \frac{K + K}{R} \in ℝ^{+}$
17	16	rpred	$⊢ φ \to \frac{K + K}{R} \in ℝ$
18		oveq2	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to P D z = P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))$
19	18	breq1d	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to (P D z \leq R \leftrightarrow P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \leq R)$
20		eleq1	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to (z \in A (K) \leftrightarrow P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K))$
21	19 20	imbi12d	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to ((P D z \leq R \to z \in A (K)) \leftrightarrow (P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \leq R \to P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K)))$
22		rabss	$⊢ \{z \in X \| P D z \leq R\} \subseteq A (K) \leftrightarrow \forall z \in X (P D z \leq R \to z \in A (K))$
23	13 22	sylib	$⊢ φ \to \forall z \in X (P D z \leq R \to z \in A (K))$
24	23	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to \forall z \in X (P D z \leq R \to z \in A (K))$
25		bnnv	$⊢ U \in CBan \to U \in NrmCVec$
26	5 25	ax-mp	$⊢ U \in NrmCVec$
27	26	a1i	$⊢ ((φ \land t \in T) \land x \in X) \to U \in NrmCVec$
28	11	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to P \in X$
29	12	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to R \in ℝ^{+}$
30	29	rpcnd	$⊢ ((φ \land t \in T) \land x \in X) \to R \in ℂ$
31		simpr	$⊢ ((φ \land t \in T) \land x \in X) \to x \in X$
32		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
33	1 32	nvscl	$⊢ (U \in NrmCVec \land R \in ℂ \land x \in X) \to R \cdot_{𝑠OLD} (U) x \in X$
34	27 30 31 33	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to R \cdot_{𝑠OLD} (U) x \in X$
35		eqid	$⊢ +_{v} (U) = +_{v} (U)$
36	1 35	nvgcl	$⊢ (U \in NrmCVec \land P \in X \land R \cdot_{𝑠OLD} (U) x \in X) \to P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X$
37	27 28 34 36	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X$
38	21 24 37	rspcdva	$⊢ ((φ \land t \in T) \land x \in X) \to (P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \leq R \to P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K))$
39	1 3	cbncms	$⊢ U \in CBan \to D \in CMet (X)$
40	5 39	ax-mp	$⊢ D \in CMet (X)$
41		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
42		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
43	40 41 42	mp2b	$⊢ D \in ∞Met (X)$
44	43	a1i	$⊢ ((φ \land t \in T) \land x \in X) \to D \in ∞Met (X)$
45		xmetsym	$⊢ (D \in ∞Met (X) \land P \in X \land P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X) \to P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) = (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) D P$
46	44 28 37 45	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) = (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) D P$
47		eqid	$⊢ -_{v} (U) = -_{v} (U)$
48		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
49	1 47 48 3	imsdval	$⊢ (U \in NrmCVec \land P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land P \in X) \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) D P = {norm}_{CV} (U) ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P)$
50	27 37 28 49	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) D P = {norm}_{CV} (U) ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P)$
51	1 35 47	nvpncan2	$⊢ (U \in NrmCVec \land P \in X \land R \cdot_{𝑠OLD} (U) x \in X) \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P = R \cdot_{𝑠OLD} (U) x$
52	27 28 34 51	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P = R \cdot_{𝑠OLD} (U) x$
53	52	fveq2d	$⊢ ((φ \land t \in T) \land x \in X) \to {norm}_{CV} (U) ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P) = {norm}_{CV} (U) (R \cdot_{𝑠OLD} (U) x)$
54	46 50 53	3eqtrd	$⊢ ((φ \land t \in T) \land x \in X) \to P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) = {norm}_{CV} (U) (R \cdot_{𝑠OLD} (U) x)$
55	29	rprege0d	$⊢ ((φ \land t \in T) \land x \in X) \to (R \in ℝ \land 0 \leq R)$
56	1 32 48	nvsge0	$⊢ (U \in NrmCVec \land (R \in ℝ \land 0 \leq R) \land x \in X) \to {norm}_{CV} (U) (R \cdot_{𝑠OLD} (U) x) = R {norm}_{CV} (U) (x)$
57	27 55 31 56	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to {norm}_{CV} (U) (R \cdot_{𝑠OLD} (U) x) = R {norm}_{CV} (U) (x)$
58	54 57	eqtrd	$⊢ ((φ \land t \in T) \land x \in X) \to P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) = R {norm}_{CV} (U) (x)$
59	30	mulid1d	$⊢ ((φ \land t \in T) \land x \in X) \to R \cdot 1 = R$
60	59	eqcomd	$⊢ ((φ \land t \in T) \land x \in X) \to R = R \cdot 1$
61	58 60	breq12d	$⊢ ((φ \land t \in T) \land x \in X) \to (P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \leq R \leftrightarrow R {norm}_{CV} (U) (x) \leq R \cdot 1)$
62	1 48	nvcl	$⊢ (U \in NrmCVec \land x \in X) \to {norm}_{CV} (U) (x) \in ℝ$
63	26 62	mpan	$⊢ x \in X \to {norm}_{CV} (U) (x) \in ℝ$
64	63	adantl	$⊢ ((φ \land t \in T) \land x \in X) \to {norm}_{CV} (U) (x) \in ℝ$
65		1red	$⊢ ((φ \land t \in T) \land x \in X) \to 1 \in ℝ$
66	64 65 29	lemul2d	$⊢ ((φ \land t \in T) \land x \in X) \to ({norm}_{CV} (U) (x) \leq 1 \leftrightarrow R {norm}_{CV} (U) (x) \leq R \cdot 1)$
67	61 66	bitr4d	$⊢ ((φ \land t \in T) \land x \in X) \to (P D (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \leq R \leftrightarrow {norm}_{CV} (U) (x) \leq 1)$
68		breq2	$⊢ k = K \to (N (t (z)) \leq k \leftrightarrow N (t (z)) \leq K)$
69	68	ralbidv	$⊢ k = K \to (\forall t \in T N (t (z)) \leq k \leftrightarrow \forall t \in T N (t (z)) \leq K)$
70	69	rabbidv	$⊢ k = K \to \{z \in X \| \forall t \in T N (t (z)) \leq k\} = \{z \in X \| \forall t \in T N (t (z)) \leq K\}$
71	1	fvexi	$⊢ X \in V$
72	71	rabex	$⊢ \{z \in X \| \forall t \in T N (t (z)) \leq K\} \in V$
73	70 9 72	fvmpt	$⊢ K \in ℕ \to A (K) = \{z \in X \| \forall t \in T N (t (z)) \leq K\}$
74	10 73	syl	$⊢ φ \to A (K) = \{z \in X \| \forall t \in T N (t (z)) \leq K\}$
75	74	eleq2d	$⊢ φ \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K) \leftrightarrow P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in \{z \in X \| \forall t \in T N (t (z)) \leq K\})$
76		2fveq3	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to N (t (z)) = N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)))$
77	76	breq1d	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to (N (t (z)) \leq K \leftrightarrow N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
78	77	ralbidv	$⊢ z = P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \to (\forall t \in T N (t (z)) \leq K \leftrightarrow \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
79	78	elrab	$⊢ P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in \{z \in X \| \forall t \in T N (t (z)) \leq K\} \leftrightarrow (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
80	75 79	syl6bb	$⊢ φ \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K) \leftrightarrow (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K))$
81	80	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in A (K) \leftrightarrow (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K))$
82	38 67 81	3imtr3d	$⊢ ((φ \land t \in T) \land x \in X) \to ({norm}_{CV} (U) (x) \leq 1 \to (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K))$
83		rsp	$⊢ \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to (t \in T \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
84	83	com12	$⊢ t \in T \to (\forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
85	84	ad2antlr	$⊢ ((φ \land t \in T) \land x \in X) \to (\forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K)$
86		xmet0	$⊢ (D \in ∞Met (X) \land P \in X) \to P D P = 0$
87	43 11 86	sylancr	$⊢ φ \to P D P = 0$
88	12	rpge0d	$⊢ φ \to 0 \leq R$
89	87 88	eqbrtrd	$⊢ φ \to P D P \leq R$
90		oveq2	$⊢ z = P \to P D z = P D P$
91	90	breq1d	$⊢ z = P \to (P D z \leq R \leftrightarrow P D P \leq R)$
92	91	elrab	$⊢ P \in \{z \in X \| P D z \leq R\} \leftrightarrow (P \in X \land P D P \leq R)$
93	11 89 92	sylanbrc	$⊢ φ \to P \in \{z \in X \| P D z \leq R\}$
94	13 93	sseldd	$⊢ φ \to P \in A (K)$
95	94 74	eleqtrd	$⊢ φ \to P \in \{z \in X \| \forall t \in T N (t (z)) \leq K\}$
96		2fveq3	$⊢ z = P \to N (t (z)) = N (t (P))$
97	96	breq1d	$⊢ z = P \to (N (t (z)) \leq K \leftrightarrow N (t (P)) \leq K)$
98	97	ralbidv	$⊢ z = P \to (\forall t \in T N (t (z)) \leq K \leftrightarrow \forall t \in T N (t (P)) \leq K)$
99	98	elrab	$⊢ P \in \{z \in X \| \forall t \in T N (t (z)) \leq K\} \leftrightarrow (P \in X \land \forall t \in T N (t (P)) \leq K)$
100	95 99	sylib	$⊢ φ \to (P \in X \land \forall t \in T N (t (P)) \leq K)$
101	100	simprd	$⊢ φ \to \forall t \in T N (t (P)) \leq K$
102	101	r19.21bi	$⊢ (φ \land t \in T) \to N (t (P)) \leq K$
103	102	adantr	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P)) \leq K$
104	7	sselda	$⊢ (φ \land t \in T) \to t \in (U BLnOp W)$
105		eqid	$⊢ IndMet (W) = IndMet (W)$
106		eqid	$⊢ MetOpen (IndMet (W)) = MetOpen (IndMet (W))$
107		eqid	$⊢ U BLnOp W = U BLnOp W$
108	3 105 4 106 107 26 6	blocn2	$⊢ t \in (U BLnOp W) \to t \in (J Cn MetOpen (IndMet (W)))$
109	4	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
110	43 109	ax-mp	$⊢ J \in TopOn (X)$
111		eqid	$⊢ BaseSet (W) = BaseSet (W)$
112	111 105	imsxmet	$⊢ W \in NrmCVec \to IndMet (W) \in ∞Met (BaseSet (W))$
113	106	mopntopon	$⊢ IndMet (W) \in ∞Met (BaseSet (W)) \to MetOpen (IndMet (W)) \in TopOn (BaseSet (W))$
114	6 112 113	mp2b	$⊢ MetOpen (IndMet (W)) \in TopOn (BaseSet (W))$
115		iscncl	$⊢ (J \in TopOn (X) \land MetOpen (IndMet (W)) \in TopOn (BaseSet (W))) \to (t \in (J Cn MetOpen (IndMet (W))) \leftrightarrow (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J)))$
116	110 114 115	mp2an	$⊢ t \in (J Cn MetOpen (IndMet (W))) \leftrightarrow (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
117	108 116	sylib	$⊢ t \in (U BLnOp W) \to (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
118	104 117	syl	$⊢ (φ \land t \in T) \to (t : X ⟶ BaseSet (W) \land \forall x \in Clsd (MetOpen (IndMet (W))) t^{-1} [x] \in Clsd (J))$
119	118	simpld	$⊢ (φ \land t \in T) \to t : X ⟶ BaseSet (W)$
120	119	adantr	$⊢ ((φ \land t \in T) \land x \in X) \to t : X ⟶ BaseSet (W)$
121	120 37	ffvelrnd	$⊢ ((φ \land t \in T) \land x \in X) \to t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \in BaseSet (W)$
122	111 2	nvcl	$⊢ (W \in NrmCVec \land t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \in BaseSet (W)) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \in ℝ$
123	6 121 122	sylancr	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \in ℝ$
124	120 28	ffvelrnd	$⊢ ((φ \land t \in T) \land x \in X) \to t (P) \in BaseSet (W)$
125	111 2	nvcl	$⊢ (W \in NrmCVec \land t (P) \in BaseSet (W)) \to N (t (P)) \in ℝ$
126	6 124 125	sylancr	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P)) \in ℝ$
127	10	nnred	$⊢ φ \to K \in ℝ$
128	127	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to K \in ℝ$
129		le2add	$⊢ ((N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \in ℝ \land N (t (P)) \in ℝ) \land (K \in ℝ \land K \in ℝ)) \to ((N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \land N (t (P)) \leq K) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K)$
130	123 126 128 128 129	syl22anc	$⊢ ((φ \land t \in T) \land x \in X) \to ((N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \land N (t (P)) \leq K) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K)$
131	103 130	mpan2d	$⊢ ((φ \land t \in T) \land x \in X) \to (N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K)$
132	52	fveq2d	$⊢ ((φ \land t \in T) \land x \in X) \to t ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P) = t (R \cdot_{𝑠OLD} (U) x)$
133	6	a1i	$⊢ ((φ \land t \in T) \land x \in X) \to W \in NrmCVec$
134		eqid	$⊢ U LnOp W = U LnOp W$
135	134 107	bloln	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t \in (U BLnOp W)) \to t \in (U LnOp W)$
136	26 6 135	mp3an12	$⊢ t \in (U BLnOp W) \to t \in (U LnOp W)$
137	104 136	syl	$⊢ (φ \land t \in T) \to t \in (U LnOp W)$
138	137	adantr	$⊢ ((φ \land t \in T) \land x \in X) \to t \in (U LnOp W)$
139		eqid	$⊢ -_{v} (W) = -_{v} (W)$
140	1 47 139 134	lnosub	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land t \in (U LnOp W)) \land (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land P \in X)) \to t ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P) = t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)$
141	27 133 138 37 28 140	syl32anc	$⊢ ((φ \land t \in T) \land x \in X) \to t ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (U) P) = t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)$
142		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
143	1 32 142 134	lnomul	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land t \in (U LnOp W)) \land (R \in ℂ \land x \in X)) \to t (R \cdot_{𝑠OLD} (U) x) = R \cdot_{𝑠OLD} (W) t (x)$
144	27 133 138 30 31 143	syl32anc	$⊢ ((φ \land t \in T) \land x \in X) \to t (R \cdot_{𝑠OLD} (U) x) = R \cdot_{𝑠OLD} (W) t (x)$
145	132 141 144	3eqtr3d	$⊢ ((φ \land t \in T) \land x \in X) \to t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P) = R \cdot_{𝑠OLD} (W) t (x)$
146	145	fveq2d	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)) = N (R \cdot_{𝑠OLD} (W) t (x))$
147	119	ffvelrnda	$⊢ ((φ \land t \in T) \land x \in X) \to t (x) \in BaseSet (W)$
148	111 142 2	nvsge0	$⊢ (W \in NrmCVec \land (R \in ℝ \land 0 \leq R) \land t (x) \in BaseSet (W)) \to N (R \cdot_{𝑠OLD} (W) t (x)) = R N (t (x))$
149	133 55 147 148	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to N (R \cdot_{𝑠OLD} (W) t (x)) = R N (t (x))$
150	146 149	eqtrd	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)) = R N (t (x))$
151	111 139 2	nvmtri	$⊢ (W \in NrmCVec \land t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) \in BaseSet (W) \land t (P) \in BaseSet (W)) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)) \leq N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P))$
152	133 121 124 151	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x)) -_{v} (W) t (P)) \leq N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P))$
153	150 152	eqbrtrrd	$⊢ ((φ \land t \in T) \land x \in X) \to R N (t (x)) \leq N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P))$
154	29	rpred	$⊢ ((φ \land t \in T) \land x \in X) \to R \in ℝ$
155	111 2	nvcl	$⊢ (W \in NrmCVec \land t (x) \in BaseSet (W)) \to N (t (x)) \in ℝ$
156	6 147 155	sylancr	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (x)) \in ℝ$
157	154 156	remulcld	$⊢ ((φ \land t \in T) \land x \in X) \to R N (t (x)) \in ℝ$
158	123 126	readdcld	$⊢ ((φ \land t \in T) \land x \in X) \to N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \in ℝ$
159	15	rpred	$⊢ φ \to K + K \in ℝ$
160	159	ad2antrr	$⊢ ((φ \land t \in T) \land x \in X) \to K + K \in ℝ$
161		letr	$⊢ (R N (t (x)) \in ℝ \land N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \in ℝ \land K + K \in ℝ) \to ((R N (t (x)) \leq N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \land N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K) \to R N (t (x)) \leq K + K)$
162	157 158 160 161	syl3anc	$⊢ ((φ \land t \in T) \land x \in X) \to ((R N (t (x)) \leq N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \land N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K) \to R N (t (x)) \leq K + K)$
163	153 162	mpand	$⊢ ((φ \land t \in T) \land x \in X) \to (N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) + N (t (P)) \leq K + K \to R N (t (x)) \leq K + K)$
164	131 163	syld	$⊢ ((φ \land t \in T) \land x \in X) \to (N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to R N (t (x)) \leq K + K)$
165	156 160 29	lemuldiv2d	$⊢ ((φ \land t \in T) \land x \in X) \to (R N (t (x)) \leq K + K \leftrightarrow N (t (x)) \leq \frac{K + K}{R})$
166	164 165	sylibd	$⊢ ((φ \land t \in T) \land x \in X) \to (N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to N (t (x)) \leq \frac{K + K}{R})$
167	85 166	syld	$⊢ ((φ \land t \in T) \land x \in X) \to (\forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K \to N (t (x)) \leq \frac{K + K}{R})$
168	167	adantld	$⊢ ((φ \land t \in T) \land x \in X) \to ((P +_{v} (U) (R \cdot_{𝑠OLD} (U) x) \in X \land \forall t \in T N (t (P +_{v} (U) (R \cdot_{𝑠OLD} (U) x))) \leq K) \to N (t (x)) \leq \frac{K + K}{R})$
169	82 168	syld	$⊢ ((φ \land t \in T) \land x \in X) \to ({norm}_{CV} (U) (x) \leq 1 \to N (t (x)) \leq \frac{K + K}{R})$
170	169	ralrimiva	$⊢ (φ \land t \in T) \to \forall x \in X ({norm}_{CV} (U) (x) \leq 1 \to N (t (x)) \leq \frac{K + K}{R})$
171	16	rpxrd	$⊢ φ \to \frac{K + K}{R} \in ℝ^{*}$
172	171	adantr	$⊢ (φ \land t \in T) \to \frac{K + K}{R} \in ℝ^{*}$
173		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
174	1 111 48 2 173 26 6	nmoubi	$⊢ (t : X ⟶ BaseSet (W) \land \frac{K + K}{R} \in ℝ^{*}) \to ((U {normOp}_{OLD} W) (t) \leq \frac{K + K}{R} \leftrightarrow \forall x \in X ({norm}_{CV} (U) (x) \leq 1 \to N (t (x)) \leq \frac{K + K}{R}))$
175	119 172 174	syl2anc	$⊢ (φ \land t \in T) \to ((U {normOp}_{OLD} W) (t) \leq \frac{K + K}{R} \leftrightarrow \forall x \in X ({norm}_{CV} (U) (x) \leq 1 \to N (t (x)) \leq \frac{K + K}{R}))$
176	170 175	mpbird	$⊢ (φ \land t \in T) \to (U {normOp}_{OLD} W) (t) \leq \frac{K + K}{R}$
177	176	ralrimiva	$⊢ φ \to \forall t \in T (U {normOp}_{OLD} W) (t) \leq \frac{K + K}{R}$
178		brralrspcev	$⊢ (\frac{K + K}{R} \in ℝ \land \forall t \in T (U {normOp}_{OLD} W) (t) \leq \frac{K + K}{R}) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d$
179	17 177 178	syl2anc	$⊢ φ \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d$

Metamath Proof Explorer

Theorem ubthlem2

Proof