This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )