Description: The Dirac bra of the zero vector. (Contributed by NM, 25-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bra0 | ⊢ ( bra ‘ 0_{ℎ} ) = ( ℋ × { 0 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hv0cl | ⊢ 0_{ℎ} ∈ ℋ | |
2 | brafval | ⊢ ( 0_{ℎ} ∈ ℋ → ( bra ‘ 0_{ℎ} ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 0_{ℎ} ) ) ) | |
3 | hi02 | ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ·_{ih} 0_{ℎ} ) = 0 ) | |
4 | 3 | mpteq2ia | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·_{ih} 0_{ℎ} ) ) = ( 𝑥 ∈ ℋ ↦ 0 ) |
5 | 2 4 | eqtrdi | ⊢ ( 0_{ℎ} ∈ ℋ → ( bra ‘ 0_{ℎ} ) = ( 𝑥 ∈ ℋ ↦ 0 ) ) |
6 | 1 5 | ax-mp | ⊢ ( bra ‘ 0_{ℎ} ) = ( 𝑥 ∈ ℋ ↦ 0 ) |
7 | fconstmpt | ⊢ ( ℋ × { 0 } ) = ( 𝑥 ∈ ℋ ↦ 0 ) | |
8 | 6 7 | eqtr4i | ⊢ ( bra ‘ 0_{ℎ} ) = ( ℋ × { 0 } ) |