# Metamath Proof Explorer

## Theorem nmfnval

Description: Value of the norm of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
2 1 supex ${⊢}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 \mathrm{V}$
3 ax-hilex ${⊢}ℋ\in \mathrm{V}$
4 cnex ${⊢}ℂ\in \mathrm{V}$
5 fveq1 ${⊢}{t}={T}\to {t}\left({y}\right)={T}\left({y}\right)$
6 5 fveq2d ${⊢}{t}={T}\to \left|{t}\left({y}\right)\right|=\left|{T}\left({y}\right)\right|$
7 6 eqeq2d ${⊢}{t}={T}\to \left({x}=\left|{t}\left({y}\right)\right|↔{x}=\left|{T}\left({y}\right)\right|\right)$
8 7 anbi2d ${⊢}{t}={T}\to \left(\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{t}\left({y}\right)\right|\right)↔\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right)$
9 8 rexbidv ${⊢}{t}={T}\to \left(\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{t}\left({y}\right)\right|\right)↔\exists {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({y}\right)\le 1\wedge {x}=\left|{T}\left({y}\right)\right|\right)\right)$
10 9 abbidv ${⊢}{t}={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\}=\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\}$
11 10 supeq1d ${⊢}{t}={T}\to 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)=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)$
12 df-nmfn ${⊢}{norm}_{\mathrm{fn}}=\left({t}\in \left({ℂ}^{ℋ}\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)\right)$
13 2 3 4 11 12 fvmptmap ${⊢}{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)$