# Metamath Proof Explorer

## Theorem nlfnval

Description: Value of the null space of a Hilbert space functional. (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nlfnval ${⊢}{T}:ℋ⟶ℂ\to \mathrm{null}\left({T}\right)={{T}}^{-1}\left[\left\{0\right\}\right]$

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 ax-hilex ${⊢}ℋ\in \mathrm{V}$
3 1 2 elmap ${⊢}{T}\in \left({ℂ}^{ℋ}\right)↔{T}:ℋ⟶ℂ$
4 cnvexg ${⊢}{T}\in \left({ℂ}^{ℋ}\right)\to {{T}}^{-1}\in \mathrm{V}$
5 imaexg ${⊢}{{T}}^{-1}\in \mathrm{V}\to {{T}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}$
6 4 5 syl ${⊢}{T}\in \left({ℂ}^{ℋ}\right)\to {{T}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}$
7 cnveq ${⊢}{t}={T}\to {{t}}^{-1}={{T}}^{-1}$
8 7 imaeq1d ${⊢}{t}={T}\to {{t}}^{-1}\left[\left\{0\right\}\right]={{T}}^{-1}\left[\left\{0\right\}\right]$
9 df-nlfn ${⊢}\mathrm{null}=\left({t}\in \left({ℂ}^{ℋ}\right)⟼{{t}}^{-1}\left[\left\{0\right\}\right]\right)$
10 8 9 fvmptg ${⊢}\left({T}\in \left({ℂ}^{ℋ}\right)\wedge {{T}}^{-1}\left[\left\{0\right\}\right]\in \mathrm{V}\right)\to \mathrm{null}\left({T}\right)={{T}}^{-1}\left[\left\{0\right\}\right]$
11 6 10 mpdan ${⊢}{T}\in \left({ℂ}^{ℋ}\right)\to \mathrm{null}\left({T}\right)={{T}}^{-1}\left[\left\{0\right\}\right]$
12 3 11 sylbir ${⊢}{T}:ℋ⟶ℂ\to \mathrm{null}\left({T}\right)={{T}}^{-1}\left[\left\{0\right\}\right]$