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 : ~H --> CC /\ A e. ( null ` T ) ) -> ( T ` A ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnlfn | |- ( T : ~H --> CC -> ( A e. ( null ` T ) <-> ( A e. ~H /\ ( T ` A ) = 0 ) ) ) |
|
| 2 | 1 | simplbda | |- ( ( T : ~H --> CC /\ A e. ( null ` T ) ) -> ( T ` A ) = 0 ) |