Metamath Proof Explorer


Theorem dfhnorm2

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

Proof

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