Theorem bloval

Description: The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bloval.3	|- N = ( U normOpOLD W )
	bloval.4	|- L = ( U LnOp W )
	bloval.5	|- B = ( U BLnOp W )
Assertion	bloval	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> B = { t e. L | ( N ` t ) < +oo } )

Proof

Step	Hyp	Ref	Expression
1		bloval.3	|- N = ( U normOpOLD W )
2		bloval.4	|- L = ( U LnOp W )
3		bloval.5	|- B = ( U BLnOp W )
4		oveq1	|- ( u = U -> ( u LnOp w ) = ( U LnOp w ) )
5		oveq1	|- ( u = U -> ( u normOpOLD w ) = ( U normOpOLD w ) )
6	5	fveq1d	|- ( u = U -> ( ( u normOpOLD w ) ` t ) = ( ( U normOpOLD w ) ` t ) )
7	6	breq1d	|- ( u = U -> ( ( ( u normOpOLD w ) ` t ) < +oo <-> ( ( U normOpOLD w ) ` t ) < +oo ) )
8	4 7	rabeqbidv	|- ( u = U -> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } = { t e. ( U LnOp w ) | ( ( U normOpOLD w ) ` t ) < +oo } )
9		oveq2	|- ( w = W -> ( U LnOp w ) = ( U LnOp W ) )
10	9 2	eqtr4di	|- ( w = W -> ( U LnOp w ) = L )
11		oveq2	|- ( w = W -> ( U normOpOLD w ) = ( U normOpOLD W ) )
12	11 1	eqtr4di	|- ( w = W -> ( U normOpOLD w ) = N )
13	12	fveq1d	|- ( w = W -> ( ( U normOpOLD w ) ` t ) = ( N ` t ) )
14	13	breq1d	|- ( w = W -> ( ( ( U normOpOLD w ) ` t ) < +oo <-> ( N ` t ) < +oo ) )
15	10 14	rabeqbidv	|- ( w = W -> { t e. ( U LnOp w ) | ( ( U normOpOLD w ) ` t ) < +oo } = { t e. L | ( N ` t ) < +oo } )
16		df-blo	|- BLnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )
17	2	ovexi	|- L e. _V
18	17	rabex	|- { t e. L | ( N ` t ) < +oo } e. _V
19	8 15 16 18	ovmpo	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U BLnOp W ) = { t e. L | ( N ` t ) < +oo } )
20	3 19	syl5eq	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> B = { t e. L | ( N ` t ) < +oo } )