Description: The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | normf | |- normh : ~H --> RR |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfhnorm2 | |- normh = ( x e. ~H |-> ( sqrt ` ( x .ih x ) ) ) |
|
| 2 | hiidrcl | |- ( x e. ~H -> ( x .ih x ) e. RR ) |
|
| 3 | hiidge0 | |- ( x e. ~H -> 0 <_ ( x .ih x ) ) |
|
| 4 | 2 3 | resqrtcld | |- ( x e. ~H -> ( sqrt ` ( x .ih x ) ) e. RR ) |
| 5 | 1 4 | fmpti | |- normh : ~H --> RR |