# Metamath Proof Explorer

## Theorem nmfnrepnf

Description: The norm of a Hilbert space functional is either real or plus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 nmfnsetre ${⊢}{T}:ℋ⟶ℂ\to \left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\}\subseteq ℝ$
2 nmfnsetn0 ${⊢}\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}=\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}=\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}=\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}=\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}=\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}=\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}=\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}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
6 nmfnval ${⊢}{T}:ℋ⟶ℂ\to {norm}_{\mathrm{fn}}\left({T}\right)=sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)$
7 6 eleq1d ${⊢}{T}:ℋ⟶ℂ\to \left({norm}_{\mathrm{fn}}\left({T}\right)\in ℝ↔sup\left(\left\{{x}|\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)\in ℝ\right)$
8 6 neeq1d ${⊢}{T}:ℋ⟶ℂ\to \left({norm}_{\mathrm{fn}}\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}=\left|{T}\left({y}\right)\right|\right)\right\},{ℝ}^{*},<\right)\ne \mathrm{+\infty }\right)$
9 5 7 8 3bitr4d ${⊢}{T}:ℋ⟶ℂ\to \left({norm}_{\mathrm{fn}}\left({T}\right)\in ℝ↔{norm}_{\mathrm{fn}}\left({T}\right)\ne \mathrm{+\infty }\right)$