Theorem nmogtmnf

Description: The norm of an operator is greater than minus 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	nmogtmnf	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> -oo < ( N ` T ) )

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		df-ne	|- ( ( N ` T ) =/= +oo <-> -. ( N ` T ) = +oo )
6	4 5	bitrdi	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> ( ( N ` T ) e. RR <-> -. ( N ` T ) = +oo ) )
7		xor3	|- ( -. ( ( N ` T ) e. RR <-> ( N ` T ) = +oo ) <-> ( ( N ` T ) e. RR <-> -. ( N ` T ) = +oo ) )
8		nbior	|- ( -. ( ( N ` T ) e. RR <-> ( N ` T ) = +oo ) -> ( ( N ` T ) e. RR \/ ( N ` T ) = +oo ) )
9	7 8	sylbir	|- ( ( ( N ` T ) e. RR <-> -. ( N ` T ) = +oo ) -> ( ( N ` T ) e. RR \/ ( N ` T ) = +oo ) )
10		mnfltxr	|- ( ( ( N ` T ) e. RR \/ ( N ` T ) = +oo ) -> -oo < ( N ` T ) )
11	6 9 10	3syl	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ T : X --> Y ) -> -oo < ( N ` T ) )