Theorem blocn

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (Contributed by NM, 25-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	blocn.8	|- C = ( IndMet ` U )
	blocn.d	|- D = ( IndMet ` W )
	blocn.j	|- J = ( MetOpen ` C )
	blocn.k	|- K = ( MetOpen ` D )
	blocn.5	|- B = ( U BLnOp W )
	blocn.u	|- U e. NrmCVec
	blocn.w	|- W e. NrmCVec
	blocn.4	|- L = ( U LnOp W )
Assertion	blocn	|- ( T e. L -> ( T e. ( J Cn K ) <-> T e. B ) )

Proof

Step	Hyp	Ref	Expression
1		blocn.8	|- C = ( IndMet ` U )
2		blocn.d	|- D = ( IndMet ` W )
3		blocn.j	|- J = ( MetOpen ` C )
4		blocn.k	|- K = ( MetOpen ` D )
5		blocn.5	|- B = ( U BLnOp W )
6		blocn.u	|- U e. NrmCVec
7		blocn.w	|- W e. NrmCVec
8		blocn.4	|- L = ( U LnOp W )
9		eleq1	|- ( T = if ( T e. L , T , ( U 0op W ) ) -> ( T e. ( J Cn K ) <-> if ( T e. L , T , ( U 0op W ) ) e. ( J Cn K ) ) )
10		eleq1	|- ( T = if ( T e. L , T , ( U 0op W ) ) -> ( T e. B <-> if ( T e. L , T , ( U 0op W ) ) e. B ) )
11	9 10	bibi12d	|- ( T = if ( T e. L , T , ( U 0op W ) ) -> ( ( T e. ( J Cn K ) <-> T e. B ) <-> ( if ( T e. L , T , ( U 0op W ) ) e. ( J Cn K ) <-> if ( T e. L , T , ( U 0op W ) ) e. B ) ) )
12		eqid	|- ( U 0op W ) = ( U 0op W )
13	12 8	0lno	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U 0op W ) e. L )
14	6 7 13	mp2an	|- ( U 0op W ) e. L
15	14	elimel	|- if ( T e. L , T , ( U 0op W ) ) e. L
16	1 2 3 4 8 5 6 7 15	blocni	|- ( if ( T e. L , T , ( U 0op W ) ) e. ( J Cn K ) <-> if ( T e. L , T , ( U 0op W ) ) e. B )
17	11 16	dedth	|- ( T e. L -> ( T e. ( J Cn K ) <-> T e. B ) )