Theorem blocn2

Description: A bounded linear operator is continuous. (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
Assertion	blocn2	|- ( T e. B -> T e. ( J Cn K ) )

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		eqid	|- ( U LnOp W ) = ( U LnOp W )
9	8 5	bloln	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> T e. ( U LnOp W ) )
10	6 7 9	mp3an12	|- ( T e. B -> T e. ( U LnOp W ) )
11	1 2 3 4 5 6 7 8	blocn	|- ( T e. ( U LnOp W ) -> ( T e. ( J Cn K ) <-> T e. B ) )
12	11	biimprd	|- ( T e. ( U LnOp W ) -> ( T e. B -> T e. ( J Cn K ) ) )
13	10 12	mpcom	|- ( T e. B -> T e. ( J Cn K ) )