Metamath Proof Explorer

Theorem brafval

Description: The bra of a vector, expressed as <. A | in Dirac notation. See df-bra . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion brafval A bra A = x x ih A


Step Hyp Ref Expression
1 oveq2 y = A x ih y = x ih A
2 1 mpteq2dv y = A x x ih y = x x ih A
3 df-bra bra = y x x ih y
4 ax-hilex V
5 4 mptex x x ih A V
6 2 3 5 fvmpt A bra A = x x ih A