This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )