Theorem hhbloi

Description: A bounded linear operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhnmo.1	|- U = <. <. +h , .h >. , normh >.
	hhblo.2	|- B = ( U BLnOp U )
Assertion	hhbloi	|- BndLinOp = B

Proof

Step	Hyp	Ref	Expression
1		hhnmo.1	|- U = <. <. +h , .h >. , normh >.
2		hhblo.2	|- B = ( U BLnOp U )
3		df-bdop	|- BndLinOp = { x e. LinOp | ( normop ` x ) < +oo }
4	1	hhnv	|- U e. NrmCVec
5		eqid	|- ( U normOpOLD U ) = ( U normOpOLD U )
6	1 5	hhnmoi	|- normop = ( U normOpOLD U )
7		eqid	|- ( U LnOp U ) = ( U LnOp U )
8	1 7	hhlnoi	|- LinOp = ( U LnOp U )
9	6 8 2	bloval	|- ( ( U e. NrmCVec /\ U e. NrmCVec ) -> B = { x e. LinOp | ( normop ` x ) < +oo } )
10	4 4 9	mp2an	|- B = { x e. LinOp | ( normop ` x ) < +oo }
11	3 10	eqtr4i	|- BndLinOp = B