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 21719 for its value and normcl 21720 for its closure. Theorems normii 21728, normiii 21732, and normiiii 21734 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 21519  . 2  
2  vx  . . 3  
3  csp 21518  . . . . 5  
4  3  cdm 4705  . . . 4 
5  4  cdm 4705  . . 3 
6  2  cv 1631  . . . . 5 
7  6, 6, 3  co 5874  . . . 4 
8  csqr 11734  . . . 4  
9  7, 8  cfv 5271  . . 3 
10  2, 5, 9  cmpt 4093  . 2 
11  1, 10  wceq 1632  1 
Colors of variables: wff set class 
This definition is referenced by: dfhnorm2 21717 
Copyright terms: Public domain  W3C validator 