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	⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝐴 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		elnlfn	⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝐴 ∈ ( null ‘ 𝑇 ) ↔ ( 𝐴 ∈ ℋ ∧ ( 𝑇 ‘ 𝐴 ) = 0 ) ) )
2	1	simplbda	⊢ ( ( 𝑇 : ℋ ⟶ ℂ ∧ 𝐴 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ 𝐴 ) = 0 )