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

Metamath Proof Explorer

Theorem nmoreltpnf

Description: The norm of any operator is real iff it is less than 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 nmoreltpnf 
|- ( ( 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 1 2 3 nmorepnf 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> ( N ` T ) =/= +oo ) )
5 1 2 3 nmoxr 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( N ` T ) e. RR* )
6 nltpnft 
 |-  ( ( N ` T ) e. RR* -> ( ( N ` T ) = +oo <-> -. ( N ` T ) < +oo ) )
7 5 6 syl 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) = +oo <-> -. ( N ` T ) < +oo ) )
8 7 necon2abid 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) < +oo <-> ( N ` T ) =/= +oo ) )
9 4 8 bitr4d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> ( N ` T ) < +oo ) )