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 ) ) ) |