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

Metamath Proof Explorer

Theorem nmopsetretHIL

Description: The set in the supremum of the operator norm definition df-nmop is a set of reals. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopsetretHIL 
|- ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
2 1 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
3 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
4 1 hhnm 
 |-  normh = ( normCV ` <. <. +h , .h >. , normh >. )
5 3 4 nmosetre 
 |-  ( ( <. <. +h , .h >. , normh >. e. NrmCVec /\ T : ~H --> ~H ) -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )
6 2 5 mpan 
 |-  ( T : ~H --> ~H -> { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( normh ` ( T ` y ) ) ) } C_ RR )