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 | ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝐴 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ·_{ih} 𝑦 ) = ( 𝑥 ·_{ih} 𝐴 ) ) | |
2 | 1 | mpteq2dv | ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝑦 ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝐴 ) ) ) |
3 | df-bra | ⊢ bra = ( 𝑦 ∈ ℋ ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝑦 ) ) ) | |
4 | ax-hilex | ⊢ ℋ ∈ V | |
5 | 4 | mptex | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝐴 ) ) ∈ V |
6 | 2 3 5 | fvmpt | ⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 𝐴 ) ) ) |