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

Metamath Proof Explorer

Theorem hhnmoi

Description: The norm of an operator in Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 
|- U = <. <. +h , .h >. , normh >.
hhnmo.2 
|- N = ( U normOpOLD U )
Assertion hhnmoi 
|- normop = N

Proof

Step Hyp Ref Expression
1 hhnmo.1 
 |-  U = <. <. +h , .h >. , normh >.
2 hhnmo.2 
 |-  N = ( U normOpOLD U )
3 df-nmop 
 |-  normop = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) )
4 1 hhnv 
 |-  U e. NrmCVec
5 1 hhba 
 |-  ~H = ( BaseSet ` U )
6 1 hhnm 
 |-  normh = ( normCV ` U )
7 5 5 6 6 2 nmoofval 
 |-  ( ( U e. NrmCVec /\ U e. NrmCVec ) -> N = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) ) )
8 4 4 7 mp2an 
 |-  N = ( t e. ( ~H ^m ~H ) |-> sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( t ` y ) ) ) } , RR* , < ) )
9 3 8 eqtr4i 
 |-  normop = N