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 ) )