Metamath Proof Explorer

Theorem nmorepnf

Description: The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-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 nmorepnf 
|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> ( N ` T ) =/= +oo ) )

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 ` W ) = ( normCV ` W )
5 2 4 nmosetre 
 |-  ( ( W e. NrmCVec /\ T : X --> Y ) -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR )
6 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
7 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
8 1 6 7 nmosetn0 
 |-  ( U e. NrmCVec -> ( ( normCV ` W ) ` ( T ` ( 0vec ` U ) ) ) e. { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } )
9 8 ne0d 
 |-  ( U e. NrmCVec -> { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } =/= (/) )
10 supxrre2 
 |-  ( ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } C_ RR /\ { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } =/= (/) ) -> ( sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) e. RR <-> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) =/= +oo ) )
11 5 9 10 syl2anr 
 |-  ( ( 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 <-> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) =/= +oo ) )
12 11 3impb 
 |-  ( ( 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 <-> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) =/= +oo ) )
13 1 2 7 4 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* , < ) )
14 13 eleq1d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) e. RR ) )
15 13 neeq1d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) =/= +oo <-> sup ( { x | E. z e. X ( ( ( normCV ` U ) ` z ) <_ 1 /\ x = ( ( normCV ` W ) ` ( T ` z ) ) ) } , RR* , < ) =/= +oo ) )
16 12 14 15 3bitr4d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> ( N ` T ) =/= +oo ) )