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