# Metamath Proof Explorer

## Theorem nmopgt0

Description: A linear Hilbert space operator that is not identically zero has a positive norm. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopgt0 ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\ne 0↔0<{norm}_{\mathrm{op}}\left({T}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nmopxr ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}$
2 nmopge0 ${⊢}{T}:ℋ⟶ℋ\to 0\le {norm}_{\mathrm{op}}\left({T}\right)$
3 0xr ${⊢}0\in {ℝ}^{*}$
4 xrleltne ${⊢}\left(0\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\wedge 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to \left(0<{norm}_{\mathrm{op}}\left({T}\right)↔{norm}_{\mathrm{op}}\left({T}\right)\ne 0\right)$
5 3 4 mp3an1 ${⊢}\left({norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\wedge 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to \left(0<{norm}_{\mathrm{op}}\left({T}\right)↔{norm}_{\mathrm{op}}\left({T}\right)\ne 0\right)$
6 1 2 5 syl2anc ${⊢}{T}:ℋ⟶ℋ\to \left(0<{norm}_{\mathrm{op}}\left({T}\right)↔{norm}_{\mathrm{op}}\left({T}\right)\ne 0\right)$
7 6 bicomd ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\ne 0↔0<{norm}_{\mathrm{op}}\left({T}\right)\right)$