Definition df-hnorm 9137

Description: Define the function for the norm of a vector of Hilbert space. See normvalt 9139 for its value and normclt 9140 for its closure. Theorems norm-i 9149, norm-ii 9153, and norm-iii 9155 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.

Assertion

Ref	Expression
df-hnorm	|- normh = {<.x, y>. | (x e. H~ /\ y = (sqr` (x .ih x)))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-hnorm

Step	Hyp	Ref	Expression
1		cno 8974	. 2 class normh
2		vx	. . . . . 6 set x
3	2	cv 1098	. . . . 5 class x
4		chil 8968	. . . . 5 class H~
5	3, 4	wcel 1105	. . . 4 wff x e. H~
6		vy	. . . . . 6 set y
7	6	cv 1098	. . . . 5 class y
8		csp 8973	. . . . . . 7 class .ih
9	3, 3, 8	co 3902	. . . . . 6 class (x .ih x)
10		csqr 6550	. . . . . 6 class sqr
11	9, 10	cfv 3145	. . . . 5 class (sqr` (x .ih x))
12	7, 11	wceq 1099	. . . 4 wff y = (sqr` (x .ih x))
13	5, 12	wa 223	. . 3 wff (x e. H~ /\ y = (sqr` (x .ih x)))
14	13, 2, 6	copab 2634	. 2 class {<.x, y>. | (x e. H~ /\ y = (sqr` (x .ih x)))}
15	1, 14	wceq 1099	1 wff normh = {<.x, y>. | (x e. H~ /\ y = (sqr` (x .ih x)))}

This definition is referenced by:  normf 9138  normvalt 9139  hilnorm 9179

Copyright terms: Public domain