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\in \mathscr{H}\to \mathrm{bra}\left(A\right)\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$$

Proof

Step	Hyp	Ref	Expression
1		bra11	$$⊢\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}$$
2		f1of	$$⊢\mathrm{bra}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathrm{LinFn}\cap \mathrm{ContFn}\to \mathrm{bra}:\mathscr{H}⟶\mathrm{LinFn}\cap \mathrm{ContFn}$$
3	1 2	ax-mp	$$⊢\mathrm{bra}:\mathscr{H}⟶\mathrm{LinFn}\cap \mathrm{ContFn}$$
4	3	ffvelrni	$$⊢A\in \mathscr{H}\to \mathrm{bra}\left(A\right)\in \left(\mathrm{LinFn}\cap \mathrm{ContFn}\right)$$