This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brafn

Description: The bra function is a functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	brafn	$⊢ A \in ℋ \to bra (A) : ℋ ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		brafval	$⊢ A \in ℋ \to bra (A) = (x \in ℋ ⟼ x \cdot_{ih} A)$
2		hicl	$⊢ (x \in ℋ \land A \in ℋ) \to x \cdot_{ih} A \in ℂ$
3	2	ancoms	$⊢ (A \in ℋ \land x \in ℋ) \to x \cdot_{ih} A \in ℂ$
4	1 3	fmpt3d	$⊢ A \in ℋ \to bra (A) : ℋ ⟶ ℂ$