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	eqtrid	\|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> B = { t e. L \| ( N ` t ) < +oo } )

Metamath Proof Explorer

Theorem bloval

Proof