Theorem elnlfn2

Description: Membership in the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	elnlfn2	$$⊢\left(T:\mathscr{H}⟶ℂ\wedge A\in \mathrm{null}\left(T\right)\right)\to T\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		elnlfn	$$⊢T:\mathscr{H}⟶ℂ\to \left(A\in \mathrm{null}\left(T\right)\leftrightarrow \left(A\in \mathscr{H}\wedge T\left(A\right)=0\right)\right)$$
2	1	simplbda	$$⊢\left(T:\mathscr{H}⟶ℂ\wedge A\in \mathrm{null}\left(T\right)\right)\to T\left(A\right)=0$$