# Metamath Proof Explorer

## 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 ℋ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)={B}{\cdot }_{\mathrm{ih}}{A}$

### Proof

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