Theorem braval

Description: A bra-ket juxtaposition, expressed as <. A | B >. in Dirac notation, equals the inner product of the vectors. Based on definition of bra in Prugovecki p. 186. (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	braval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \mathrm{bra}\left(A\right)\left(B\right)=B{\cdot }_{\mathrm{ih}}A$$

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	1	fveq1d	$$⊢A\in \mathscr{H}\to \mathrm{bra}\left(A\right)\left(B\right)=\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}A\right)\left(B\right)$$
3		oveq1	$$⊢x=B\to x{\cdot }_{\mathrm{ih}}A=B{\cdot }_{\mathrm{ih}}A$$
4		eqid	$$⊢\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}A\right)=\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}A\right)$$
5		ovex	$$⊢B{\cdot }_{\mathrm{ih}}A\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢B\in \mathscr{H}\to \left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}A\right)\left(B\right)=B{\cdot }_{\mathrm{ih}}A$$
7	2 6	sylan9eq	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \mathrm{bra}\left(A\right)\left(B\right)=B{\cdot }_{\mathrm{ih}}A$$