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