Theorem brabn

Description: The bra of a vector is a bounded functional. (Contributed by NM, 26-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	brabn	⊢ ( 𝐴 ∈ ℋ → ( normfn ‘ ( bra ‘ 𝐴 ) ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		branmfn	⊢ ( 𝐴 ∈ ℋ → ( normfn ‘ ( bra ‘ 𝐴 ) ) = ( normℎ ‘ 𝐴 ) )
2		normcl	⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
3	1 2	eqeltrd	⊢ ( 𝐴 ∈ ℋ → ( normfn ‘ ( bra ‘ 𝐴 ) ) ∈ ℝ )