# 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}:ℋ⟶ℋ\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 nmoprepnf ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }\right)$
2 df-ne ${⊢}{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }↔¬{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }$
3 1 2 syl6bb ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔¬{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)$
4 xor3 ${⊢}¬\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)↔\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔¬{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)$
5 nbior ${⊢}¬\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\vee {norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)$
6 4 5 sylbir ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔¬{norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\vee {norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)$
7 mnfltxr ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ\vee {norm}_{\mathrm{op}}\left({T}\right)=\mathrm{+\infty }\right)\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({T}\right)$
8 3 6 7 3syl ${⊢}{T}:ℋ⟶ℋ\to \mathrm{-\infty }<{norm}_{\mathrm{op}}\left({T}\right)$