# Metamath Proof Explorer

## Theorem nmoprepnf

Description: The norm of a Hilbert space operator is either real or plus infinity. (Contributed by NM, 5-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmoprepnf ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }\right)$

### Proof

Step Hyp Ref Expression
1 nmopsetretHIL ${⊢}{T}:ℋ⟶ℋ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\subseteq ℝ$
2 nmopsetn0 ${⊢}{norm}_{ℎ}\left({T}\left({0}_{ℎ}\right)\right)\in \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}$
3 2 ne0ii ${⊢}\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\ne \varnothing$
4 supxrre2 ${⊢}\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\subseteq ℝ\wedge \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\}\ne \varnothing \right)\to \left(sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\in ℝ↔sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
5 1 3 4 sylancl ${⊢}{T}:ℋ⟶ℋ\to \left(sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\in ℝ↔sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
6 nmopval ${⊢}{T}:ℋ⟶ℋ\to {norm}_{\mathrm{op}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)$
7 6 eleq1d ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\in ℝ\right)$
8 6 neeq1d ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }↔sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}={norm}_{ℎ}\left({T}\left({y}\right)\right)\right)\right\},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
9 5 7 8 3bitr4d ${⊢}{T}:ℋ⟶ℋ\to \left({norm}_{\mathrm{op}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{op}}\left({T}\right)\ne \mathrm{+\infty }\right)$