Metamath Proof Explorer

Theorem normcl

Description: Real closure of the norm of a vector. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion normcl 
|- ( A e. ~H -> ( normh ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 normf 
 |-  normh : ~H --> RR
2 1 ffvelrni 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )