Metamath Proof Explorer

Theorem 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 = ( normCV ` W )
ubth.3 
|- M = ( U normOpOLD W )
Assertion ubth 
|- ( ( U e. CBan /\ W e. NrmCVec /\ T C_ ( U BLnOp W ) ) -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( M ` t ) <_ d ) )

Proof

Step Hyp Ref Expression
1 ubth.1 
 |-  X = ( BaseSet ` U )
2 ubth.2 
 |-  N = ( normCV ` W )
3 ubth.3 
 |-  M = ( U normOpOLD W )
4 oveq1 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( U BLnOp W ) = ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) )
5 4 sseq2d 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( T C_ ( U BLnOp W ) <-> T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) ) )
6 fveq2 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( BaseSet ` U ) = ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) )
7 1 6 eqtrid 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> X = ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) )
8 7 raleqdv 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c ) )
9 oveq1 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( U normOpOLD W ) = ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) )
10 3 9 eqtrid 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> M = ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) )
11 10 fveq1d 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( M ` t ) = ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) )
12 11 breq1d 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( ( M ` t ) <_ d <-> ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) )
13 12 rexralbidv 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( E. d e. RR A. t e. T ( M ` t ) <_ d <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) )
14 8 13 bibi12d 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( M ` t ) <_ d ) <-> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) ) )
15 5 14 imbi12d 
 |-  ( U = if ( U e. CBan , U , <. <. + , x. >. , abs >. ) -> ( ( T C_ ( U BLnOp W ) -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( M ` t ) <_ d ) ) <-> ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) -> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) ) ) )
16 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) = ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
17 16 sseq2d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) <-> T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) )
18 fveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( normCV ` W ) = ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
19 2 18 eqtrid 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> N = ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
20 19 fveq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( N ` ( t ` x ) ) = ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) )
21 20 breq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( N ` ( t ` x ) ) <_ c <-> ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c ) )
22 21 rexralbidv 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. c e. RR A. t e. T ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c ) )
23 22 ralbidv 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c ) )
24 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) = ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
25 24 fveq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) = ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) )
26 25 breq1d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d <-> ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) <_ d ) )
27 26 rexralbidv 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) <_ d ) )
28 23 27 bibi12d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) <-> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) <_ d ) ) )
29 17 28 imbi12d 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp W ) -> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD W ) ` t ) <_ d ) ) <-> ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) -> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) <_ d ) ) ) )
30 eqid 
 |-  ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) = ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) )
31 eqid 
 |-  ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
32 eqid 
 |-  ( IndMet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) = ( IndMet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) )
33 eqid 
 |-  ( MetOpen ` ( IndMet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) ) = ( MetOpen ` ( IndMet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) )
34 eqid 
 |-  <. <. + , x. >. , abs >. = <. <. + , x. >. , abs >.
35 34 cnbn 
 |-  <. <. + , x. >. , abs >. e. CBan
36 35 elimel 
 |-  if ( U e. CBan , U , <. <. + , x. >. , abs >. ) e. CBan
37 elimnvu 
 |-  if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) e. NrmCVec
38 id 
 |-  ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) -> T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
39 30 31 32 33 36 37 38 ubthlem3 
 |-  ( T C_ ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) BLnOp if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) -> ( A. x e. ( BaseSet ` if ( U e. CBan , U , <. <. + , x. >. , abs >. ) ) E. c e. RR A. t e. T ( ( normCV ` if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( ( if ( U e. CBan , U , <. <. + , x. >. , abs >. ) normOpOLD if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ` t ) <_ d ) )
40 15 29 39 dedth2h 
 |-  ( ( U e. CBan /\ W e. NrmCVec ) -> ( T C_ ( U BLnOp W ) -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( M ` t ) <_ d ) ) )
41 40 3impia 
 |-  ( ( U e. CBan /\ W e. NrmCVec /\ T C_ ( U BLnOp W ) ) -> ( A. x e. X E. c e. RR A. t e. T ( N ` ( t ` x ) ) <_ c <-> E. d e. RR A. t e. T ( M ` t ) <_ d ) )