Metamath Proof Explorer

Theorem nmopub2tHIL

Description: An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

Ref Expression
Assertion nmopub2tHIL 
|- ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )

Proof

Step Hyp Ref Expression
1 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
2 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
3 2 hhnm 
 |-  normh = ( normCV ` <. <. +h , .h >. , normh >. )
4 eqid 
 |-  ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. ) = ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. )
5 2 4 hhnmoi 
 |-  normop = ( <. <. +h , .h >. , normh >. normOpOLD <. <. +h , .h >. , normh >. )
6 2 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
7 1 1 3 3 5 6 6 nmoub2i 
 |-  ( ( T : ~H --> ~H /\ ( A e. RR /\ 0 <_ A ) /\ A. x e. ~H ( normh ` ( T ` x ) ) <_ ( A x. ( normh ` x ) ) ) -> ( normop ` T ) <_ A )