Theorem bracl

Description: Closure of the bra function. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	bracl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		brafn	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) : ℋ ⟶ ℂ )
2	1	ffvelrnda	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( bra ‘ 𝐴 ) ‘ 𝐵 ) ∈ ℂ )