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 ⊢ T : ℋ ⟶ ℂ ∧ A ∈ null ⁡ T → T ⁡ A = 0

Proof

Step Hyp Ref Expression
1 elnlfn ⊢ T : ℋ ⟶ ℂ → A ∈ null ⁡ T ↔ A ∈ ℋ ∧ T ⁡ A = 0
2 1 simplbda ⊢ T : ℋ ⟶ ℂ ∧ A ∈ null ⁡ T → T ⁡ A = 0