# Metamath Proof Explorer

## Theorem nmopge0

Description: The norm of any Hilbert space operator is nonnegative. (Contributed by NM, 9-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopge0 ${⊢}{T}:ℋ⟶ℋ\to 0\le {norm}_{\mathrm{op}}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
2 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {0}_{ℎ}\in ℋ\right)\to {T}\left({0}_{ℎ}\right)\in ℋ$
3 1 2 mpan2 ${⊢}{T}:ℋ⟶ℋ\to {T}\left({0}_{ℎ}\right)\in ℋ$
4 normge0 ${⊢}{T}\left({0}_{ℎ}\right)\in ℋ\to 0\le {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)$
5 3 4 syl ${⊢}{T}:ℋ⟶ℋ\to 0\le {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)$
6 norm0 ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)=0$
7 0le1 ${⊢}0\le 1$
8 6 7 eqbrtri ${⊢}{norm}_{ℎ}\left({0}_{ℎ}\right)\le 1$
9 nmoplb ${⊢}\left({T}:ℋ⟶ℋ\wedge {0}_{ℎ}\in ℋ\wedge {norm}_{ℎ}\left({0}_{ℎ}\right)\le 1\right)\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
10 1 8 9 mp3an23 ${⊢}{T}:ℋ⟶ℋ\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)$
11 normcl ${⊢}{T}\left({0}_{ℎ}\right)\in ℋ\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in ℝ$
12 3 11 syl ${⊢}{T}:ℋ⟶ℋ\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in ℝ$
13 12 rexrd ${⊢}{T}:ℋ⟶ℋ\to {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in {ℝ}^{*}$
14 nmopxr ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}$
15 0xr ${⊢}0\in {ℝ}^{*}$
16 xrletr ${⊢}\left(0\in {ℝ}^{*}\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\right)\to \left(\left(0\le {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)$
17 15 16 mp3an1 ${⊢}\left({norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in {ℝ}^{*}\wedge {norm}_{\mathrm{op}}\left({T}\right)\in {ℝ}^{*}\right)\to \left(\left(0\le {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)$
18 13 14 17 syl2anc ${⊢}{T}:ℋ⟶ℋ\to \left(\left(0\le {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\wedge {norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\le {norm}_{\mathrm{op}}\left({T}\right)\right)\to 0\le {norm}_{\mathrm{op}}\left({T}\right)\right)$
19 5 10 18 mp2and ${⊢}{T}:ℋ⟶ℋ\to 0\le {norm}_{\mathrm{op}}\left({T}\right)$