Theorem nmfnsetre

Description: The set in the supremum of the functional norm definition df-nmfn is a set of reals. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmfnsetre	$$⊢T:\mathscr{H}⟶ℂ\to \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=\left|T\left(y\right)\right|\right)\right\}\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	$$⊢\left(T:\mathscr{H}⟶ℂ\wedge y\in \mathscr{H}\right)\to T\left(y\right)\in ℂ$$
2	1	abscld	$$⊢\left(T:\mathscr{H}⟶ℂ\wedge y\in \mathscr{H}\right)\to \left|T\left(y\right)\right|\in ℝ$$
3		eleq1	$$⊢x=\left|T\left(y\right)\right|\to \left(x\in ℝ\leftrightarrow \left|T\left(y\right)\right|\in ℝ\right)$$
4	2 3	imbitrrid	$$⊢x=\left|T\left(y\right)\right|\to \left(\left(T:\mathscr{H}⟶ℂ\wedge y\in \mathscr{H}\right)\to x\in ℝ\right)$$
5	4	impcom	$$⊢\left(\left(T:\mathscr{H}⟶ℂ\wedge y\in \mathscr{H}\right)\wedge x=\left|T\left(y\right)\right|\right)\to x\in ℝ$$
6	5	adantrl	$$⊢\left(\left(T:\mathscr{H}⟶ℂ\wedge y\in \mathscr{H}\right)\wedge \left({norm}_{ℎ}\left(y\right)\le 1\wedge x=\left|T\left(y\right)\right|\right)\right)\to x\in ℝ$$
7	6	rexlimdva2	$$⊢T:\mathscr{H}⟶ℂ\to \left(\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=\left|T\left(y\right)\right|\right)\to x\in ℝ\right)$$
8	7	abssdv	$$⊢T:\mathscr{H}⟶ℂ\to \left\{x|\exists y\in \mathscr{H}\left({norm}_{ℎ}\left(y\right)\le 1\wedge x=\left|T\left(y\right)\right|\right)\right\}\subseteq ℝ$$