ubthlem3

Description: Lemma for ubth . Prove the reverse implication, using nmblolbi . (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$
Assertion	ubthlem3	$⊢ φ \to (\forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \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		fveq1	$⊢ u = t \to u (z) = t (z)$
9	8	fveq2d	$⊢ u = t \to N (u (z)) = N (t (z))$
10	9	breq1d	$⊢ u = t \to (N (u (z)) \leq d \leftrightarrow N (t (z)) \leq d)$
11	10	cbvralvw	$⊢ \forall u \in T N (u (z)) \leq d \leftrightarrow \forall t \in T N (t (z)) \leq d$
12		breq2	$⊢ d = c \to (N (t (z)) \leq d \leftrightarrow N (t (z)) \leq c)$
13	12	ralbidv	$⊢ d = c \to (\forall t \in T N (t (z)) \leq d \leftrightarrow \forall t \in T N (t (z)) \leq c)$
14	11 13	bitrid	$⊢ d = c \to (\forall u \in T N (u (z)) \leq d \leftrightarrow \forall t \in T N (t (z)) \leq c)$
15	14	cbvrexvw	$⊢ \exists d \in ℝ \forall u \in T N (u (z)) \leq d \leftrightarrow \exists c \in ℝ \forall t \in T N (t (z)) \leq c$
16		2fveq3	$⊢ z = x \to N (t (z)) = N (t (x))$
17	16	breq1d	$⊢ z = x \to (N (t (z)) \leq c \leftrightarrow N (t (x)) \leq c)$
18	17	rexralbidv	$⊢ z = x \to (\exists c \in ℝ \forall t \in T N (t (z)) \leq c \leftrightarrow \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
19	15 18	bitrid	$⊢ z = x \to (\exists d \in ℝ \forall u \in T N (u (z)) \leq d \leftrightarrow \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
20	19	cbvralvw	$⊢ \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d \leftrightarrow \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
21	7	adantr	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to T \subseteq U BLnOp W$
22	20	bilani	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
23		fveq1	$⊢ u = t \to u (d) = t (d)$
24	23	fveq2d	$⊢ u = t \to N (u (d)) = N (t (d))$
25	24	breq1d	$⊢ u = t \to (N (u (d)) \leq m \leftrightarrow N (t (d)) \leq m)$
26	25	cbvralvw	$⊢ \forall u \in T N (u (d)) \leq m \leftrightarrow \forall t \in T N (t (d)) \leq m$
27		2fveq3	$⊢ d = z \to N (t (d)) = N (t (z))$
28	27	breq1d	$⊢ d = z \to (N (t (d)) \leq m \leftrightarrow N (t (z)) \leq m)$
29	28	ralbidv	$⊢ d = z \to (\forall t \in T N (t (d)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq m)$
30	26 29	bitrid	$⊢ d = z \to (\forall u \in T N (u (d)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq m)$
31	30	cbvrabv	$⊢ \{d \in X \| \forall u \in T N (u (d)) \leq m\} = \{z \in X \| \forall t \in T N (t (z)) \leq m\}$
32		breq2	$⊢ m = k \to (N (t (z)) \leq m \leftrightarrow N (t (z)) \leq k)$
33	32	ralbidv	$⊢ m = k \to (\forall t \in T N (t (z)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq k)$
34	33	rabbidv	$⊢ m = k \to \{z \in X \| \forall t \in T N (t (z)) \leq m\} = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
35	31 34	eqtrid	$⊢ m = k \to \{d \in X \| \forall u \in T N (u (d)) \leq m\} = \{z \in X \| \forall t \in T N (t (z)) \leq k\}$
36	35	cbvmptv	$⊢ (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) = (k \in ℕ ⟼ \{z \in X \| \forall t \in T N (t (z)) \leq k\})$
37	1 2 3 4 5 6 21 22 36	ubthlem1	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to \exists n \in ℕ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n)$
38	7	ad3antrrr	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to T \subseteq U BLnOp W$
39	22	ad2antrr	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
40		simplrl	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to n \in ℕ$
41		simplrr	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to y \in X$
42		simprl	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to r \in ℝ^{+}$
43		simprr	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n)$
44	1 2 3 4 5 6 38 39 36 40 41 42 43	ubthlem2	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land (r \in ℝ^{+} \land \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n))) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d$
45	44	expr	$⊢ (((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \land r \in ℝ^{+}) \to (\{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$
46	45	rexlimdva	$⊢ ((φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \land (n \in ℕ \land y \in X)) \to (\exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$
47	46	rexlimdvva	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to (\exists n \in ℕ \exists y \in X \exists r \in ℝ^{+} \{z \in X \| y D z \leq r\} \subseteq (m \in ℕ ⟼ \{d \in X \| \forall u \in T N (u (d)) \leq m\}) (n) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$
48	37 47	mpd	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d$
49	48	ex	$⊢ φ \to (\forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$
50	20 49	biimtrrid	$⊢ φ \to (\forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c \to \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$
51		simpr	$⊢ (φ \land d \in ℝ) \to d \in ℝ$
52		bnnv	$⊢ U \in CBan \to U \in NrmCVec$
53	5 52	ax-mp	$⊢ U \in NrmCVec$
54		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
55	1 54	nvcl	$⊢ (U \in NrmCVec \land x \in X) \to {norm}_{CV} (U) (x) \in ℝ$
56	53 55	mpan	$⊢ x \in X \to {norm}_{CV} (U) (x) \in ℝ$
57		remulcl	$⊢ (d \in ℝ \land {norm}_{CV} (U) (x) \in ℝ) \to d {norm}_{CV} (U) (x) \in ℝ$
58	51 56 57	syl2an	$⊢ ((φ \land d \in ℝ) \land x \in X) \to d {norm}_{CV} (U) (x) \in ℝ$
59	7	sselda	$⊢ (φ \land t \in T) \to t \in (U BLnOp W)$
60	59	adantlr	$⊢ ((φ \land d \in ℝ) \land t \in T) \to t \in (U BLnOp W)$
61	60	ad2ant2r	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to t \in (U BLnOp W)$
62		eqid	$⊢ BaseSet (W) = BaseSet (W)$
63		eqid	$⊢ U BLnOp W = U BLnOp W$
64	1 62 63	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t \in (U BLnOp W)) \to t : X ⟶ BaseSet (W)$
65	53 6 64	mp3an12	$⊢ t \in (U BLnOp W) \to t : X ⟶ BaseSet (W)$
66	61 65	syl	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to t : X ⟶ BaseSet (W)$
67		simplr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to x \in X$
68	66 67	ffvelcdmd	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to t (x) \in BaseSet (W)$
69	62 2	nvcl	$⊢ (W \in NrmCVec \land t (x) \in BaseSet (W)) \to N (t (x)) \in ℝ$
70	6 69	mpan	$⊢ t (x) \in BaseSet (W) \to N (t (x)) \in ℝ$
71	68 70	syl	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to N (t (x)) \in ℝ$
72		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
73	1 62 72	nmoxr	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t : X ⟶ BaseSet (W)) \to (U {normOp}_{OLD} W) (t) \in ℝ^{*}$
74	53 6 73	mp3an12	$⊢ t : X ⟶ BaseSet (W) \to (U {normOp}_{OLD} W) (t) \in ℝ^{*}$
75	66 74	syl	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) \in ℝ^{*}$
76		simpllr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to d \in ℝ$
77	1 62 72	nmogtmnf	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t : X ⟶ BaseSet (W)) \to −∞ < (U {normOp}_{OLD} W) (t)$
78	53 6 77	mp3an12	$⊢ t : X ⟶ BaseSet (W) \to −∞ < (U {normOp}_{OLD} W) (t)$
79	66 78	syl	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to −∞ < (U {normOp}_{OLD} W) (t)$
80		simprr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) \leq d$
81		xrre	$⊢ (((U {normOp}_{OLD} W) (t) \in ℝ^{*} \land d \in ℝ) \land (−∞ < (U {normOp}_{OLD} W) (t) \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) \in ℝ$
82	75 76 79 80 81	syl22anc	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) \in ℝ$
83	56	ad2antlr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to {norm}_{CV} (U) (x) \in ℝ$
84		remulcl	$⊢ ((U {normOp}_{OLD} W) (t) \in ℝ \land {norm}_{CV} (U) (x) \in ℝ) \to (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x) \in ℝ$
85	82 83 84	syl2anc	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x) \in ℝ$
86	58	adantr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to d {norm}_{CV} (U) (x) \in ℝ$
87	1 54 2 72 63 53 6	nmblolbi	$⊢ (t \in (U BLnOp W) \land x \in X) \to N (t (x)) \leq (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x)$
88	61 67 87	syl2anc	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to N (t (x)) \leq (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x)$
89	1 54	nvge0	$⊢ (U \in NrmCVec \land x \in X) \to 0 \leq {norm}_{CV} (U) (x)$
90	53 89	mpan	$⊢ x \in X \to 0 \leq {norm}_{CV} (U) (x)$
91	56 90	jca	$⊢ x \in X \to ({norm}_{CV} (U) (x) \in ℝ \land 0 \leq {norm}_{CV} (U) (x))$
92	91	ad2antlr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to ({norm}_{CV} (U) (x) \in ℝ \land 0 \leq {norm}_{CV} (U) (x))$
93		lemul1a	$⊢ (((U {normOp}_{OLD} W) (t) \in ℝ \land d \in ℝ \land ({norm}_{CV} (U) (x) \in ℝ \land 0 \leq {norm}_{CV} (U) (x))) \land (U {normOp}_{OLD} W) (t) \leq d) \to (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x) \leq d {norm}_{CV} (U) (x)$
94	82 76 92 80 93	syl31anc	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x) \leq d {norm}_{CV} (U) (x)$
95	71 85 86 88 94	letrd	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to N (t (x)) \leq d {norm}_{CV} (U) (x)$
96	95	expr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land t \in T) \to ((U {normOp}_{OLD} W) (t) \leq d \to N (t (x)) \leq d {norm}_{CV} (U) (x))$
97	96	ralimdva	$⊢ ((φ \land d \in ℝ) \land x \in X) \to (\forall t \in T (U {normOp}_{OLD} W) (t) \leq d \to \forall t \in T N (t (x)) \leq d {norm}_{CV} (U) (x))$
98		brralrspcev	$⊢ (d {norm}_{CV} (U) (x) \in ℝ \land \forall t \in T N (t (x)) \leq d {norm}_{CV} (U) (x)) \to \exists c \in ℝ \forall t \in T N (t (x)) \leq c$
99	58 97 98	syl6an	$⊢ ((φ \land d \in ℝ) \land x \in X) \to (\forall t \in T (U {normOp}_{OLD} W) (t) \leq d \to \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
100	99	ralrimdva	$⊢ (φ \land d \in ℝ) \to (\forall t \in T (U {normOp}_{OLD} W) (t) \leq d \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
101	100	rexlimdva	$⊢ φ \to (\exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d \to \forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
102	50 101	impbid	$⊢ φ \to (\forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (U {normOp}_{OLD} W) (t) \leq d)$

Metamath Proof Explorer

Theorem ubthlem3

Proof