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 = x x ih 0
3 hi02 x x ih 0 = 0
4 3 mpteq2ia x x ih 0 = x 0
5 2 4 syl6eq 0 bra 0 = x 0
6 1 5 ax-mp bra 0 = x 0
7 fconstmpt × 0 = x 0
8 6 7 eqtr4i bra 0 = × 0