Metamath Proof Explorer


Theorem nmopgtmnf

Description: The norm of a Hilbert space operator is not minus infinity. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopgtmnf T : −∞ < norm op T

Proof

Step Hyp Ref Expression
1 nmoprepnf T : norm op T norm op T +∞
2 df-ne norm op T +∞ ¬ norm op T = +∞
3 1 2 bitrdi T : norm op T ¬ norm op T = +∞
4 xor3 ¬ norm op T norm op T = +∞ norm op T ¬ norm op T = +∞
5 nbior ¬ norm op T norm op T = +∞ norm op T norm op T = +∞
6 4 5 sylbir norm op T ¬ norm op T = +∞ norm op T norm op T = +∞
7 mnfltxr norm op T norm op T = +∞ −∞ < norm op T
8 3 6 7 3syl T : −∞ < norm op T