ubth

Description: Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let T be a collection of bounded linear operators on a Banach space. If, for every vector x , the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of Kreyszig p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle . (Contributed by NM, 7-Nov-2007) (Proof shortened by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ubth.1	$⊢ X = BaseSet (U)$
	ubth.2	$⊢ N = {norm}_{CV} (W)$
	ubth.3	$⊢ M = U {normOp}_{OLD} W$
Assertion	ubth	$⊢ (U \in CBan \land W \in NrmCVec \land T \subseteq U BLnOp W) \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 M (t) \leq d)$

Proof

Step	Hyp	Ref	Expression
1		ubth.1	$⊢ X = BaseSet (U)$
2		ubth.2	$⊢ N = {norm}_{CV} (W)$
3		ubth.3	$⊢ M = U {normOp}_{OLD} W$
4		oveq1	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to U BLnOp W = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W$
5	4	sseq2d	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to (T \subseteq U BLnOp W \leftrightarrow T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W)$
6		fveq2	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to BaseSet (U) = BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩))$
7	1 6	eqtrid	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to X = BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩))$
8	7	raleqdv	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to (\forall x \in X \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c)$
9		oveq1	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to U {normOp}_{OLD} W = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W$
10	3 9	eqtrid	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to M = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W$
11	10	fveq1d	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to M (t) = (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t)$
12	11	breq1d	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to (M (t) \leq d \leftrightarrow (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d)$
13	12	rexralbidv	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to (\exists d \in ℝ \forall t \in T M (t) \leq d \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d)$
14	8 13	bibi12d	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \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 M (t) \leq d) \leftrightarrow (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d))$
15	5 14	imbi12d	$⊢ U = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \to ((T \subseteq U BLnOp W \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 M (t) \leq d)) \leftrightarrow (T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W \to (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d)))$
16		oveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
17	16	sseq2d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W \leftrightarrow T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
18		fveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to {norm}_{CV} (W) = {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
19	2 18	eqtrid	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to N = {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
20	19	fveq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to N (t (x)) = {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x))$
21	20	breq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (N (t (x)) \leq c \leftrightarrow {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c)$
22	21	rexralbidv	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (\exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists c \in ℝ \forall t \in T {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c)$
23	22	ralbidv	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c)$
24		oveq2	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W = if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
25	24	fveq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) = (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t)$
26	25	breq1d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to ((if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d \leftrightarrow (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t) \leq d)$
27	26	rexralbidv	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (\exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t) \leq d)$
28	23 27	bibi12d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to ((\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d) \leftrightarrow (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t) \leq d))$
29	17 28	imbi12d	$⊢ W = if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to ((T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp W \to (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T N (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} W) (t) \leq d)) \leftrightarrow (T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t) \leq d)))$
30		eqid	$⊢ BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) = BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩))$
31		eqid	$⊢ {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) = {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩))$
32		eqid	$⊢ IndMet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) = IndMet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩))$
33		eqid	$⊢ MetOpen (IndMet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩))) = MetOpen (IndMet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)))$
34		eqid	$⊢ ⟨⟨+ \times⟩, abs⟩ = ⟨⟨+ \times⟩, abs⟩$
35	34	cnbn	$⊢ ⟨⟨+ \times⟩, abs⟩ \in CBan$
36	35	elimel	$⊢ if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) \in CBan$
37		elimnvu	$⊢ if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \in NrmCVec$
38		id	$⊢ T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)$
39	30 31 32 33 36 37 38	ubthlem3	$⊢ T \subseteq if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) BLnOp if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩) \to (\forall x \in BaseSet (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩)) \exists c \in ℝ \forall t \in T {norm}_{CV} (if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t (x)) \leq c \leftrightarrow \exists d \in ℝ \forall t \in T (if (U \in CBan, U, ⟨⟨+ \times⟩, abs⟩) {normOp}_{OLD} if (W \in NrmCVec, W, ⟨⟨+ \times⟩, abs⟩)) (t) \leq d)$
40	15 29 39	dedth2h	$⊢ (U \in CBan \land W \in NrmCVec) \to (T \subseteq U BLnOp W \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 M (t) \leq d))$
41	40	3impia	$⊢ (U \in CBan \land W \in NrmCVec \land T \subseteq U BLnOp W) \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 M (t) \leq d)$

Metamath Proof Explorer

Theorem ubth

Proof