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 norm = x dom dom ih x ih x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cno class norm
1 vx setvar x
2 csp class ih
3 2 cdm class dom ih
4 3 cdm class dom dom ih
5 csqrt class
6 1 cv setvar x
7 6 6 2 co class x ih x
8 7 5 cfv class x ih x
9 1 4 8 cmpt class x dom dom ih x ih x
10 0 9 wceq wff norm = x dom dom ih x ih x