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

Metamath Proof Explorer

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