This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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