Hilbert Space Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > HSE Home > Th. List > dfhnorm  Unicode version 
Description: Define the function for the norm of a vector of Hilbert space. See normval 22579 for its value and normcl 22580 for its closure. Theorems normii 22588, normiii 22592, and normiiii 22594 show it has the expected properties of a norm. In the literature, the norm of is usually written " ", but we use function notation to take advantage of our existing theorems about functions. Definition of norm in [Beran] p. 96. (Contributed by NM, 6Jun2008.) (New usage is discouraged.) 
Ref  Expression 

dfhnorm 
Step  Hyp  Ref  Expression 

1  cno 22379  . 2  
2  vx  . . 3  
3  csp 22378  . . . . 5  
4  3  cdm 4837  . . . 4 
5  4  cdm 4837  . . 3 
6  2  cv 1648  . . . . 5 
7  6, 6, 3  co 6040  . . . 4 
8  csqr 11993  . . . 4  
9  7, 8  cfv 5413  . . 3 
10  2, 5, 9  cmpt 4226  . 2 
11  1, 10  wceq 1649  1 
Colors of variables: wff set class 
This definition is referenced by: dfhnorm2 22577 
Copyright terms: Public domain  W3C validator 