Definition df-hnorm 5074

Description: Define the function for the norm of a vector of Hilbert space. See normvalt 5075 for its value and normclt 5076 for its closure. Theorems norm-i 5083, norm-ii 5086, and norm-iii 5087 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	⊢ norm = {⟨x, y⟩∣(x ∈ ℋ ∧ y = (√ ‘(x ·i x)))}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-hnorm

Step	Hyp	Ref	Expression
1		cno 4964	. 2 class norm
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		chil 4958	. . . . 5 class ℋ
5	3, 4	wcel 1092	. . . 4 wff x ∈ ℋ
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		csp 4963	. . . . . . 7 class ·i
9	3, 3, 8	co 3001	. . . . . 6 class (x ·i x)
10		csqr 4727	. . . . . 6 class √
11	9, 10	cfv 2422	. . . . 5 class (√ ‘(x ·i x))
12	7, 11	wceq 1091	. . . 4 wff y = (√ ‘(x ·i x))
13	5, 12	wa 196	. . 3 wff (x ∈ ℋ ∧ y = (√ ‘(x ·i x)))
14	13, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ ℋ ∧ y = (√ ‘(x ·i x)))}
15	1, 14	wceq 1091	1 wff norm = {⟨x, y⟩∣(x ∈ ℋ ∧ y = (√ ‘(x ·i x)))}

This definition is referenced by:  normvalt 5075

metamath.org