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 A B bra A B = B ih A


Step Hyp Ref Expression
1 brafval A bra A = x x ih A
2 1 fveq1d A bra A B = x x ih A B
3 oveq1 x = B x ih A = B ih A
4 eqid x x ih A = x x ih A
5 ovex B ih A V
6 3 4 5 fvmpt B x x ih A B = B ih A
7 2 6 sylan9eq A B bra A B = B ih A