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 ` 0h ) = ( ~H X. { 0 } )

Proof

Step Hyp Ref Expression
1 ax-hv0cl
 |-  0h e. ~H
2 brafval
 |-  ( 0h e. ~H -> ( bra ` 0h ) = ( x e. ~H |-> ( x .ih 0h ) ) )
3 hi02
 |-  ( x e. ~H -> ( x .ih 0h ) = 0 )
4 3 mpteq2ia
 |-  ( x e. ~H |-> ( x .ih 0h ) ) = ( x e. ~H |-> 0 )
5 2 4 syl6eq
 |-  ( 0h e. ~H -> ( bra ` 0h ) = ( x e. ~H |-> 0 ) )
6 1 5 ax-mp
 |-  ( bra ` 0h ) = ( x e. ~H |-> 0 )
7 fconstmpt
 |-  ( ~H X. { 0 } ) = ( x e. ~H |-> 0 )
8 6 7 eqtr4i
 |-  ( bra ` 0h ) = ( ~H X. { 0 } )