Description: Alternate definition of the norm of a vector of Hilbert space. Definition of norm in Beran p. 96. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | dfhnorm2 | |- normh = ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-hnorm | |- normh = ( x e. dom dom .ih |-> ( sqrt ` ( x .ih x ) ) ) |
|
2 | ax-hfi | |- .ih : ( ~H X. ~H ) --> CC |
|
3 | 2 | fdmi | |- dom .ih = ( ~H X. ~H ) |
4 | 3 | dmeqi | |- dom dom .ih = dom ( ~H X. ~H ) |
5 | dmxpid | |- dom ( ~H X. ~H ) = ~H |
|
6 | 4 5 | eqtr2i | |- ~H = dom dom .ih |
7 | 6 | mpteq1i | |- ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) ) = ( x e. dom dom .ih |-> ( sqrt ` ( x .ih x ) ) ) |
8 | 1 7 | eqtr4i | |- normh = ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) ) |