Definition df-hnorm

Description: Define the function for the norm of a vector of Hilbert space. See normval for its value and normcl for its closure. Theorems norm-i-i , norm-ii-i , and norm-iii-i show it has the expected properties of a norm. In the literature, the norm of A is usually written "|| A ||", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in Beran p. 96. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hnorm	$$⊢{norm}_{ℎ}=\left(x\in \mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cno	$$class{norm}_{ℎ}$$
1		vx	$$setvarx$$
2		csp	$$class{\cdot }_{\mathrm{ih}}$$
3	2	cdm	$$class\mathrm{dom}{\cdot }_{\mathrm{ih}}$$
4	3	cdm	$$class\mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}$$
5		csqrt	$$class\surd$$
6	1	cv	$$setvarx$$
7	6 6 2	co	$$class\left(x{\cdot }_{\mathrm{ih}}x\right)$$
8	7 5	cfv	$$class\sqrt{x{\cdot }_{\mathrm{ih}}x}$$
9	1 4 8	cmpt	$$class\left(x\in \mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$
10	0 9	wceq	$$wff{norm}_{ℎ}=\left(x\in \mathrm{dom}\mathrm{dom}{\cdot }_{\mathrm{ih}}⟼\sqrt{x{\cdot }_{\mathrm{ih}}x}\right)$$