Theorem brabn

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\in \mathscr{H}\to {norm}_{\mathrm{fn}}\left(\mathrm{bra}\left(A\right)\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		branmfn	$$⊢A\in \mathscr{H}\to {norm}_{\mathrm{fn}}\left(\mathrm{bra}\left(A\right)\right)={norm}_{ℎ}\left(A\right)$$
2		normcl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)\in ℝ$$
3	1 2	eqeltrd	$$⊢A\in \mathscr{H}\to {norm}_{\mathrm{fn}}\left(\mathrm{bra}\left(A\right)\right)\in ℝ$$