Metamath Proof Explorer

Theorem nmoxr

Description: The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 
|- X = ( BaseSet ` U )
nmoxr.2 
|- Y = ( BaseSet ` W )
nmoxr.3 
|- N = ( U normOpOLD W )
Assertion nmoxr 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )

Proof

Step Hyp Ref Expression
1 nmoxr.1 
 |-  X = ( BaseSet ` U )
2 nmoxr.2 
 |-  Y = ( BaseSet ` W )
3 nmoxr.3 
 |-  N = ( U normOpOLD W )
4 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
5 eqid 
 |-  ( normCV ` W ) = ( normCV ` W )
6 1 2 4 5 3 nmooval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) = sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) )
7 2 5 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR )
8 ressxr 
 |-  RR C_ RR*
9 7 8 sstrdi 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* )
10 supxrcl 
 |-  ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR* -> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) e. RR* )
11 9 10 syl 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) e. RR* )
12 11 3adant1 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) e. RR* )
13 6 12 eqeltrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )