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 )