Metamath Proof Explorer

Theorem brabn

Description: The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

Ref Expression
Assertion brabn 
|- ( A e. ~H -> ( normfn ` ( bra ` A ) ) e. RR )

Proof

Step Hyp Ref Expression
1 branmfn 
 |-  ( A e. ~H -> ( normfn ` ( bra ` A ) ) = ( normh ` A ) )
2 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
3 1 2 eqeltrd 
 |-  ( A e. ~H -> ( normfn ` ( bra ` A ) ) e. RR )