Theorem brafn

Description: The bra function is a functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	brafn	$$⊢A\in \mathscr{H}\to \mathrm{bra}\left(A\right):\mathscr{H}⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		brafval	$$⊢A\in \mathscr{H}\to \mathrm{bra}\left(A\right)=\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}A\right)$$
2		hicl	$$⊢\left(x\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}A\in ℂ$$
3	2	ancoms	$$⊢\left(A\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}A\in ℂ$$
4	1 3	fmpt3d	$$⊢A\in \mathscr{H}\to \mathrm{bra}\left(A\right):\mathscr{H}⟶ℂ$$