Metamath Proof Explorer


Theorem bra0

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 } )

Proof

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 syl6eq ( 0 ∈ ℋ → ( bra ‘ 0 ) = ( 𝑥 ∈ ℋ ↦ 0 ) )
6 1 5 ax-mp ( bra ‘ 0 ) = ( 𝑥 ∈ ℋ ↦ 0 )
7 fconstmpt ( ℋ × { 0 } ) = ( 𝑥 ∈ ℋ ↦ 0 )
8 6 7 eqtr4i ( bra ‘ 0 ) = ( ℋ × { 0 } )