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