Definition df-hnorm 8776

Description: Define the function for the norm of a vector of Hilbert space. See normvalt 8929 for its value and normclt 8930 for its closure. Theorems norm-i 8939, norm-ii 8943, and norm-iii 8945 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 ∈ dom dom ·ih ⋀ y = (√ ‘(x ·ih x)))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-hnorm

Step	Hyp	Ref	Expression
1		cno 8733	. 2 class normh
2		vx	. . . . . 6 set x
3	2	cv 953	. . . . 5 class x
4		csp 8732	. . . . . . 7 class ·ih
5	4	cdm 3165	. . . . . 6 class dom ·ih
6	5	cdm 3165	. . . . 5 class dom dom ·ih
7	3, 6	wcel 956	. . . 4 wff x ∈ dom dom ·ih
8		vy	. . . . . 6 set y
9	8	cv 953	. . . . 5 class y
10	3, 3, 4	co 3954	. . . . . 6 class (x ·ih x)
11		csqr 6607	. . . . . 6 class √
12	10, 11	cfv 3177	. . . . 5 class (√ ‘(x ·ih x))
13	9, 12	wceq 954	. . . 4 wff y = (√ ‘(x ·ih x))
14	7, 13	wa 223	. . 3 wff (x ∈ dom dom ·ih ⋀ y = (√ ‘(x ·ih x)))
15	14, 2, 8	copab 2661	. 2 class {⟨x, y⟩∣(x ∈ dom dom ·ih ⋀ y = (√ ‘(x ·ih x)))}
16	1, 15	wceq 954	1 wff normh = {⟨x, y⟩∣(x ∈ dom dom ·ih ⋀ y = (√ ‘(x ·ih x)))}

This definition is referenced by:  dfhnorm2 8927

Copyright terms: Public domain