Metamath Proof Explorer


Theorem bracnln

Description: A bra is a continuous linear functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bracnln
|- ( A e. ~H -> ( bra ` A ) e. ( LinFn i^i ContFn ) )

Proof

Step Hyp Ref Expression
1 bra11
 |-  bra : ~H -1-1-onto-> ( LinFn i^i ContFn )
2 f1of
 |-  ( bra : ~H -1-1-onto-> ( LinFn i^i ContFn ) -> bra : ~H --> ( LinFn i^i ContFn ) )
3 1 2 ax-mp
 |-  bra : ~H --> ( LinFn i^i ContFn )
4 3 ffvelrni
 |-  ( A e. ~H -> ( bra ` A ) e. ( LinFn i^i ContFn ) )