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	⊢ normℎ = ( 𝑥 ∈ dom dom ·ih ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cno	⊢ normℎ
1		vx	⊢ 𝑥
2		csp	⊢ ·ih
3	2	cdm	⊢ dom ·ih
4	3	cdm	⊢ dom dom ·ih
5		csqrt	⊢ √
6	1	cv	⊢ 𝑥
7	6 6 2	co	⊢ ( 𝑥 ·ih 𝑥 )
8	7 5	cfv	⊢ ( √ ‘ ( 𝑥 ·ih 𝑥 ) )
9	1 4 8	cmpt	⊢ ( 𝑥 ∈ dom dom ·ih ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )
10	0 9	wceq	⊢ normℎ = ( 𝑥 ∈ dom dom ·ih ↦ ( √ ‘ ( 𝑥 ·ih 𝑥 ) ) )