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	syl5bb	$⊢ 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	syl5bb	$⊢ 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		simpr	$⊢ (φ \land \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d) \to \forall z \in X \exists d \in ℝ \forall u \in T N (u (z)) \leq d$
23	22 20	sylib	$⊢ (φ \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$
24		fveq1	$⊢ u = t \to u (d) = t (d)$
25	24	fveq2d	$⊢ u = t \to N (u (d)) = N (t (d))$
26	25	breq1d	$⊢ u = t \to (N (u (d)) \leq m \leftrightarrow N (t (d)) \leq m)$
27	26	cbvralvw	$⊢ \forall u \in T N (u (d)) \leq m \leftrightarrow \forall t \in T N (t (d)) \leq m$
28		2fveq3	$⊢ d = z \to N (t (d)) = N (t (z))$
29	28	breq1d	$⊢ d = z \to (N (t (d)) \leq m \leftrightarrow N (t (z)) \leq m)$
30	29	ralbidv	$⊢ d = z \to (\forall t \in T N (t (d)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq m)$
31	27 30	syl5bb	$⊢ d = z \to (\forall u \in T N (u (d)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq m)$
32	31	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\}$
33		breq2	$⊢ m = k \to (N (t (z)) \leq m \leftrightarrow N (t (z)) \leq k)$
34	33	ralbidv	$⊢ m = k \to (\forall t \in T N (t (z)) \leq m \leftrightarrow \forall t \in T N (t (z)) \leq k)$
35	34	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\}$
36	32 35	syl5eq	$⊢ 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\}$
37	36	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\})$
38	1 2 3 4 5 6 21 23 37	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)$
39	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$
40	23	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$
41		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 ℕ$
42		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$
43		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 ℝ^{+}$
44		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)$
45	1 2 3 4 5 6 39 40 37 41 42 43 44	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$
46	45	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)$
47	46	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)$
48	47	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)$
49	38 48	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$
50	49	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)$
51	20 50	syl5bir	$⊢ φ \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)$
52		simpr	$⊢ (φ \land d \in ℝ) \to d \in ℝ$
53		bnnv	$⊢ U \in CBan \to U \in NrmCVec$
54	5 53	ax-mp	$⊢ U \in NrmCVec$
55		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
56	1 55	nvcl	$⊢ (U \in NrmCVec \land x \in X) \to {norm}_{CV} (U) (x) \in ℝ$
57	54 56	mpan	$⊢ x \in X \to {norm}_{CV} (U) (x) \in ℝ$
58		remulcl	$⊢ (d \in ℝ \land {norm}_{CV} (U) (x) \in ℝ) \to d {norm}_{CV} (U) (x) \in ℝ$
59	52 57 58	syl2an	$⊢ ((φ \land d \in ℝ) \land x \in X) \to d {norm}_{CV} (U) (x) \in ℝ$
60	7	sselda	$⊢ (φ \land t \in T) \to t \in (U BLnOp W)$
61	60	adantlr	$⊢ ((φ \land d \in ℝ) \land t \in T) \to t \in (U BLnOp W)$
62	61	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)$
63		eqid	$⊢ BaseSet (W) = BaseSet (W)$
64		eqid	$⊢ U BLnOp W = U BLnOp W$
65	1 63 64	blof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t \in (U BLnOp W)) \to t : X ⟶ BaseSet (W)$
66	54 6 65	mp3an12	$⊢ t \in (U BLnOp W) \to t : X ⟶ BaseSet (W)$
67	62 66	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)$
68		simplr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to x \in X$
69	67 68	ffvelrnd	$⊢ (((φ \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)$
70	63 2	nvcl	$⊢ (W \in NrmCVec \land t (x) \in BaseSet (W)) \to N (t (x)) \in ℝ$
71	6 70	mpan	$⊢ t (x) \in BaseSet (W) \to N (t (x)) \in ℝ$
72	69 71	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 ℝ$
73		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
74	1 63 73	nmoxr	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t : X ⟶ BaseSet (W)) \to (U {normOp}_{OLD} W) (t) \in ℝ^{*}$
75	54 6 74	mp3an12	$⊢ t : X ⟶ BaseSet (W) \to (U {normOp}_{OLD} W) (t) \in ℝ^{*}$
76	67 75	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 ℝ^{*}$
77		simpllr	$⊢ (((φ \land d \in ℝ) \land x \in X) \land (t \in T \land (U {normOp}_{OLD} W) (t) \leq d)) \to d \in ℝ$
78	1 63 73	nmogtmnf	$⊢ (U \in NrmCVec \land W \in NrmCVec \land t : X ⟶ BaseSet (W)) \to −∞ < (U {normOp}_{OLD} W) (t)$
79	54 6 78	mp3an12	$⊢ t : X ⟶ BaseSet (W) \to −∞ < (U {normOp}_{OLD} W) (t)$
80	67 79	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)$
81		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$
82		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 ℝ$
83	76 77 80 81 82	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 ℝ$
84	57	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 ℝ$
85		remulcl	$⊢ ((U {normOp}_{OLD} W) (t) \in ℝ \land {norm}_{CV} (U) (x) \in ℝ) \to (U {normOp}_{OLD} W) (t) {norm}_{CV} (U) (x) \in ℝ$
86	83 84 85	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 ℝ$
87	59	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 ℝ$
88	1 55 2 73 64 54 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)$
89	62 68 88	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)$
90	1 55	nvge0	$⊢ (U \in NrmCVec \land x \in X) \to 0 \leq {norm}_{CV} (U) (x)$
91	54 90	mpan	$⊢ x \in X \to 0 \leq {norm}_{CV} (U) (x)$
92	57 91	jca	$⊢ x \in X \to ({norm}_{CV} (U) (x) \in ℝ \land 0 \leq {norm}_{CV} (U) (x))$
93	92	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))$
94		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)$
95	83 77 93 81 94	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)$
96	72 86 87 89 95	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)$
97	96	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))$
98	97	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))$
99		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$
100	59 98 99	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)$
101	100	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)$
102	101	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)$
103	51 102	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