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 | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐵 ·ih 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brafval | ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) ) | |
| 2 | 1 | fveq1d | ⊢ ( 𝐴 ∈ ℋ → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) ‘ 𝐵 ) ) |
| 3 | oveq1 | ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ·ih 𝐴 ) = ( 𝐵 ·ih 𝐴 ) ) | |
| 4 | eqid | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) | |
| 5 | ovex | ⊢ ( 𝐵 ·ih 𝐴 ) ∈ V | |
| 6 | 3 4 5 | fvmpt | ⊢ ( 𝐵 ∈ ℋ → ( ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) ‘ 𝐵 ) = ( 𝐵 ·ih 𝐴 ) ) |
| 7 | 2 6 | sylan9eq | ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐵 ·ih 𝐴 ) ) |