Theorem normf

Description: The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	normf	$$⊢{norm}_{ℎ}:\mathscr{H}⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dfhnorm2	$$⊢{norm}_{ℎ}=\left(x\in \mathscr{H}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$
2		hiidrcl	$$⊢x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}x\in ℝ$$
3		hiidge0	$$⊢x\in \mathscr{H}\to 0\le x{\cdot }_{\mathrm{ih}}x$$
4	2 3	resqrtcld	$$⊢x\in \mathscr{H}\to \sqrt{x{\cdot }_{\mathrm{ih}}x}\in ℝ$$
5	1 4	fmpti	$$⊢{norm}_{ℎ}:\mathscr{H}⟶ℝ$$