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	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		brafval	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) = ( 𝑥 ∈ ℋ ↦ ( 𝑥 ·ih 𝐴 ) ) )
2		hicl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝑥 ·ih 𝐴 ) ∈ ℂ )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑥 ·ih 𝐴 ) ∈ ℂ )
4	1 3	fmpt3d	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ )