Theorem bracnln

Description: A bra is a continuous linear functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	bracnln	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) ∈ ( LinFn ∩ ContFn ) )

Proof

Step	Hyp	Ref	Expression
1		bra11	⊢ bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn )
2		f1of	⊢ ( bra : ℋ –1-1-onto→ ( LinFn ∩ ContFn ) → bra : ℋ ⟶ ( LinFn ∩ ContFn ) )
3	1 2	ax-mp	⊢ bra : ℋ ⟶ ( LinFn ∩ ContFn )
4	3	ffvelrni	⊢ ( 𝐴 ∈ ℋ → ( bra ‘ 𝐴 ) ∈ ( LinFn ∩ ContFn ) )