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_{ℎ}) = ℋ \times \{0\}$

Proof

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