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 )