Metamath Proof Explorer

Theorem brafval

Description: The bra of a vector, expressed as <. A | in Dirac notation. See df-bra . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	brafval	$⊢ A \in ℋ \to bra (A) = (x \in ℋ ⟼ x \cdot_{ih} A)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ y = A \to x \cdot_{ih} y = x \cdot_{ih} A$
2	1	mpteq2dv	$⊢ y = A \to (x \in ℋ ⟼ x \cdot_{ih} y) = (x \in ℋ ⟼ x \cdot_{ih} A)$
3		df-bra	$⊢ bra = (y \in ℋ ⟼ (x \in ℋ ⟼ x \cdot_{ih} y))$
4		ax-hilex	$⊢ ℋ \in V$
5	4	mptex	$⊢ (x \in ℋ ⟼ x \cdot_{ih} A) \in V$
6	2 3 5	fvmpt	$⊢ A \in ℋ \to bra (A) = (x \in ℋ ⟼ x \cdot_{ih} A)$