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	$$⊢\mathrm{bra}\left(0_{ℎ}\right)=\mathscr{H}\times \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		brafval	$$⊢0_{ℎ}\in \mathscr{H}\to \mathrm{bra}\left(0_{ℎ}\right)=\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}{0}_{ℎ}\right)$$
3		hi02	$$⊢x\in \mathscr{H}\to x{\cdot }_{\mathrm{ih}}{0}_{ℎ}=0$$
4	3	mpteq2ia	$$⊢\left(x\in \mathscr{H}⟼x{\cdot }_{\mathrm{ih}}{0}_{ℎ}\right)=\left(x\in \mathscr{H}⟼0\right)$$
5	2 4	eqtrdi	$$⊢0_{ℎ}\in \mathscr{H}\to \mathrm{bra}\left(0_{ℎ}\right)=\left(x\in \mathscr{H}⟼0\right)$$
6	1 5	ax-mp	$$⊢\mathrm{bra}\left(0_{ℎ}\right)=\left(x\in \mathscr{H}⟼0\right)$$
7		fconstmpt	$$⊢\mathscr{H}\times \left\{0\right\}=\left(x\in \mathscr{H}⟼0\right)$$
8	6 7	eqtr4i	$$⊢\mathrm{bra}\left(0_{ℎ}\right)=\mathscr{H}\times \left\{0\right\}$$