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	|- normh = ( x e. dom dom .ih |-> ( sqrt ` ( x .ih x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cno	|- normh
1		vx	|- x
2		csp	|- .ih
3	2	cdm	|- dom .ih
4	3	cdm	|- dom dom .ih
5		csqrt	|- sqrt
6	1	cv	|- x
7	6 6 2	co	|- ( x .ih x )
8	7 5	cfv	|- ( sqrt ` ( x .ih x ) )
9	1 4 8	cmpt	|- ( x e. dom dom .ih |-> ( sqrt ` ( x .ih x ) ) )
10	0 9	wceq	|- normh = ( x e. dom dom .ih |-> ( sqrt ` ( x .ih x ) ) )