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 normOp OLD W
Assertion nmogtmnf U NrmCVec W NrmCVec T : X Y −∞ < N T

Proof

Step Hyp Ref Expression
1 nmoxr.1 X = BaseSet U
2 nmoxr.2 Y = BaseSet W
3 nmoxr.3 N = U normOp OLD W
4 1 2 3 nmorepnf U NrmCVec W NrmCVec T : X Y N T N T +∞
5 df-ne N T +∞ ¬ N T = +∞
6 4 5 bitrdi U NrmCVec W NrmCVec T : X Y N T ¬ N T = +∞
7 xor3 ¬ N T N T = +∞ N T ¬ N T = +∞
8 nbior ¬ N T N T = +∞ N T N T = +∞
9 7 8 sylbir N T ¬ N T = +∞ N T N T = +∞
10 mnfltxr N T N T = +∞ −∞ < N T
11 6 9 10 3syl U NrmCVec W NrmCVec T : X Y −∞ < N T