This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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