blocni

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (Contributed by NM, 18-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$
Assertion	blocni	$⊢ T \in (J Cn K) \leftrightarrow 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		eqid	$⊢ BaseSet (U) = BaseSet (U)$
11		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
12	10 11	nvzcl	$⊢ U \in NrmCVec \to 0_{vec} (U) \in BaseSet (U)$
13	7 12	ax-mp	$⊢ 0_{vec} (U) \in BaseSet (U)$
14	10 1	imsmet	$⊢ U \in NrmCVec \to C \in Met (BaseSet (U))$
15	7 14	ax-mp	$⊢ C \in Met (BaseSet (U))$
16		metxmet	$⊢ C \in Met (BaseSet (U)) \to C \in ∞Met (BaseSet (U))$
17	15 16	ax-mp	$⊢ C \in ∞Met (BaseSet (U))$
18	3	mopntopon	$⊢ C \in ∞Met (BaseSet (U)) \to J \in TopOn (BaseSet (U))$
19	17 18	ax-mp	$⊢ J \in TopOn (BaseSet (U))$
20	19	toponunii	$⊢ BaseSet (U) = ⋃ J$
21	20	cncnpi	$⊢ (T \in (J Cn K) \land 0_{vec} (U) \in BaseSet (U)) \to T \in (J CnP K) (0_{vec} (U))$
22	13 21	mpan2	$⊢ T \in (J Cn K) \to T \in (J CnP K) (0_{vec} (U))$
23	1 2 3 4 5 6 7 8 9 10	blocnilem	$⊢ (0_{vec} (U) \in BaseSet (U) \land T \in (J CnP K) (0_{vec} (U))) \to T \in B$
24	13 22 23	sylancr	$⊢ T \in (J Cn K) \to T \in B$
25		eleq1	$⊢ T = U 0_{op} W \to (T \in (J Cn K) \leftrightarrow U 0_{op} W \in (J Cn K))$
26		simprr	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to y \in ℝ^{+}$
27		eqid	$⊢ BaseSet (W) = BaseSet (W)$
28		eqid	$⊢ U {normOp}_{OLD} W = U {normOp}_{OLD} W$
29	10 27 28 6	nmblore	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in B) \to (U {normOp}_{OLD} W) (T) \in ℝ$
30	7 8 29	mp3an12	$⊢ T \in B \to (U {normOp}_{OLD} W) (T) \in ℝ$
31		eqid	$⊢ U 0_{op} W = U 0_{op} W$
32	28 31 5	nmlnogt0	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to (T \neq U 0_{op} W \leftrightarrow 0 < (U {normOp}_{OLD} W) (T))$
33	7 8 9 32	mp3an	$⊢ T \neq U 0_{op} W \leftrightarrow 0 < (U {normOp}_{OLD} W) (T)$
34	33	biimpi	$⊢ T \neq U 0_{op} W \to 0 < (U {normOp}_{OLD} W) (T)$
35	30 34	anim12i	$⊢ (T \in B \land T \neq U 0_{op} W) \to ((U {normOp}_{OLD} W) (T) \in ℝ \land 0 < (U {normOp}_{OLD} W) (T))$
36		elrp	$⊢ (U {normOp}_{OLD} W) (T) \in ℝ^{+} \leftrightarrow ((U {normOp}_{OLD} W) (T) \in ℝ \land 0 < (U {normOp}_{OLD} W) (T))$
37	35 36	sylibr	$⊢ (T \in B \land T \neq U 0_{op} W) \to (U {normOp}_{OLD} W) (T) \in ℝ^{+}$
38	37	adantr	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to (U {normOp}_{OLD} W) (T) \in ℝ^{+}$
39	26 38	rpdivcld	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to \frac{y}{(U {normOp}_{OLD} W) (T)} \in ℝ^{+}$
40		simprl	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to x \in BaseSet (U)$
41		metcl	$⊢ (C \in Met (BaseSet (U)) \land x \in BaseSet (U) \land w \in BaseSet (U)) \to x C w \in ℝ$
42	15 41	mp3an1	$⊢ (x \in BaseSet (U) \land w \in BaseSet (U)) \to x C w \in ℝ$
43	40 42	sylan	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to x C w \in ℝ$
44		simplrr	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to y \in ℝ^{+}$
45	44	rpred	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to y \in ℝ$
46	35	ad2antrr	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to ((U {normOp}_{OLD} W) (T) \in ℝ \land 0 < (U {normOp}_{OLD} W) (T))$
47		ltmuldiv2	$⊢ (x C w \in ℝ \land y \in ℝ \land ((U {normOp}_{OLD} W) (T) \in ℝ \land 0 < (U {normOp}_{OLD} W) (T))) \to ((U {normOp}_{OLD} W) (T) (x C w) < y \leftrightarrow x C w < \frac{y}{(U {normOp}_{OLD} W) (T)})$
48	43 45 46 47	syl3anc	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to ((U {normOp}_{OLD} W) (T) (x C w) < y \leftrightarrow x C w < \frac{y}{(U {normOp}_{OLD} W) (T)})$
49		id	$⊢ (T \in B \land x \in BaseSet (U)) \to (T \in B \land x \in BaseSet (U))$
50	49	ad2ant2r	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to (T \in B \land x \in BaseSet (U))$
51	10 27 1 2 28 6 7 8	blometi	$⊢ (T \in B \land x \in BaseSet (U) \land w \in BaseSet (U)) \to T (x) D T (w) \leq (U {normOp}_{OLD} W) (T) (x C w)$
52	51	3expa	$⊢ ((T \in B \land x \in BaseSet (U)) \land w \in BaseSet (U)) \to T (x) D T (w) \leq (U {normOp}_{OLD} W) (T) (x C w)$
53	50 52	sylan	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to T (x) D T (w) \leq (U {normOp}_{OLD} W) (T) (x C w)$
54	10 27 5	lnof	$⊢ (U \in NrmCVec \land W \in NrmCVec \land T \in L) \to T : BaseSet (U) ⟶ BaseSet (W)$
55	7 8 9 54	mp3an	$⊢ T : BaseSet (U) ⟶ BaseSet (W)$
56	55	ffvelrni	$⊢ x \in BaseSet (U) \to T (x) \in BaseSet (W)$
57	55	ffvelrni	$⊢ w \in BaseSet (U) \to T (w) \in BaseSet (W)$
58	27 2	imsmet	$⊢ W \in NrmCVec \to D \in Met (BaseSet (W))$
59	8 58	ax-mp	$⊢ D \in Met (BaseSet (W))$
60		metcl	$⊢ (D \in Met (BaseSet (W)) \land T (x) \in BaseSet (W) \land T (w) \in BaseSet (W)) \to T (x) D T (w) \in ℝ$
61	59 60	mp3an1	$⊢ (T (x) \in BaseSet (W) \land T (w) \in BaseSet (W)) \to T (x) D T (w) \in ℝ$
62	56 57 61	syl2an	$⊢ (x \in BaseSet (U) \land w \in BaseSet (U)) \to T (x) D T (w) \in ℝ$
63	40 62	sylan	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to T (x) D T (w) \in ℝ$
64		remulcl	$⊢ ((U {normOp}_{OLD} W) (T) \in ℝ \land x C w \in ℝ) \to (U {normOp}_{OLD} W) (T) (x C w) \in ℝ$
65	30 42 64	syl2an	$⊢ (T \in B \land (x \in BaseSet (U) \land w \in BaseSet (U))) \to (U {normOp}_{OLD} W) (T) (x C w) \in ℝ$
66	65	anassrs	$⊢ ((T \in B \land x \in BaseSet (U)) \land w \in BaseSet (U)) \to (U {normOp}_{OLD} W) (T) (x C w) \in ℝ$
67	66	adantllr	$⊢ (((T \in B \land T \neq U 0_{op} W) \land x \in BaseSet (U)) \land w \in BaseSet (U)) \to (U {normOp}_{OLD} W) (T) (x C w) \in ℝ$
68	67	adantlrr	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to (U {normOp}_{OLD} W) (T) (x C w) \in ℝ$
69		lelttr	$⊢ (T (x) D T (w) \in ℝ \land (U {normOp}_{OLD} W) (T) (x C w) \in ℝ \land y \in ℝ) \to ((T (x) D T (w) \leq (U {normOp}_{OLD} W) (T) (x C w) \land (U {normOp}_{OLD} W) (T) (x C w) < y) \to T (x) D T (w) < y)$
70	63 68 45 69	syl3anc	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to ((T (x) D T (w) \leq (U {normOp}_{OLD} W) (T) (x C w) \land (U {normOp}_{OLD} W) (T) (x C w) < y) \to T (x) D T (w) < y)$
71	53 70	mpand	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to ((U {normOp}_{OLD} W) (T) (x C w) < y \to T (x) D T (w) < y)$
72	48 71	sylbird	$⊢ (((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \land w \in BaseSet (U)) \to (x C w < \frac{y}{(U {normOp}_{OLD} W) (T)} \to T (x) D T (w) < y)$
73	72	ralrimiva	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to \forall w \in BaseSet (U) (x C w < \frac{y}{(U {normOp}_{OLD} W) (T)} \to T (x) D T (w) < y)$
74		breq2	$⊢ z = \frac{y}{(U {normOp}_{OLD} W) (T)} \to (x C w < z \leftrightarrow x C w < \frac{y}{(U {normOp}_{OLD} W) (T)})$
75	74	rspceaimv	$⊢ (\frac{y}{(U {normOp}_{OLD} W) (T)} \in ℝ^{+} \land \forall w \in BaseSet (U) (x C w < \frac{y}{(U {normOp}_{OLD} W) (T)} \to T (x) D T (w) < y)) \to \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y)$
76	39 73 75	syl2anc	$⊢ ((T \in B \land T \neq U 0_{op} W) \land (x \in BaseSet (U) \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y)$
77	76	ralrimivva	$⊢ (T \in B \land T \neq U 0_{op} W) \to \forall x \in BaseSet (U) \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y)$
78	77 55	jctil	$⊢ (T \in B \land T \neq U 0_{op} W) \to (T : BaseSet (U) ⟶ BaseSet (W) \land \forall x \in BaseSet (U) \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y))$
79		metxmet	$⊢ D \in Met (BaseSet (W)) \to D \in ∞Met (BaseSet (W))$
80	59 79	ax-mp	$⊢ D \in ∞Met (BaseSet (W))$
81	3 4	metcn	$⊢ (C \in ∞Met (BaseSet (U)) \land D \in ∞Met (BaseSet (W))) \to (T \in (J Cn K) \leftrightarrow (T : BaseSet (U) ⟶ BaseSet (W) \land \forall x \in BaseSet (U) \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y)))$
82	17 80 81	mp2an	$⊢ T \in (J Cn K) \leftrightarrow (T : BaseSet (U) ⟶ BaseSet (W) \land \forall x \in BaseSet (U) \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in BaseSet (U) (x C w < z \to T (x) D T (w) < y))$
83	78 82	sylibr	$⊢ (T \in B \land T \neq U 0_{op} W) \to T \in (J Cn K)$
84		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
85	10 84 31	0ofval	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to U 0_{op} W = BaseSet (U) \times \{0_{vec} (W)\}$
86	7 8 85	mp2an	$⊢ U 0_{op} W = BaseSet (U) \times \{0_{vec} (W)\}$
87	4	mopntopon	$⊢ D \in ∞Met (BaseSet (W)) \to K \in TopOn (BaseSet (W))$
88	80 87	ax-mp	$⊢ K \in TopOn (BaseSet (W))$
89	27 84	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in BaseSet (W)$
90	8 89	ax-mp	$⊢ 0_{vec} (W) \in BaseSet (W)$
91		cnconst2	$⊢ (J \in TopOn (BaseSet (U)) \land K \in TopOn (BaseSet (W)) \land 0_{vec} (W) \in BaseSet (W)) \to BaseSet (U) \times \{0_{vec} (W)\} \in (J Cn K)$
92	19 88 90 91	mp3an	$⊢ BaseSet (U) \times \{0_{vec} (W)\} \in (J Cn K)$
93	86 92	eqeltri	$⊢ U 0_{op} W \in (J Cn K)$
94	93	a1i	$⊢ T \in B \to U 0_{op} W \in (J Cn K)$
95	25 83 94	pm2.61ne	$⊢ T \in B \to T \in (J Cn K)$
96	24 95	impbii	$⊢ T \in (J Cn K) \leftrightarrow T \in B$

Metamath Proof Explorer

Theorem blocni

Proof