[proofplan]
We differentiate the eigenvalue equation as an identity in $\mathcal{H}$. The graph-norm hypotheses ensure that both $H(\lambda)$ and $\psi(\lambda)$ vary in Banach spaces where the operator-valued product rule is valid. After differentiating, we take the Hilbert-space [inner product](/page/Inner%20Product) with the normalized eigenvector and use self-adjointness to move $H(\lambda)$ from $\psi'(\lambda)$ onto $\psi(\lambda)$. The two terms involving $\psi'(\lambda)$ then match and cancel, leaving exactly the Hellmann-Feynman formula.
[/proofplan]
[step:Differentiate the eigenvalue equation in $\mathcal{H}$]
Fix $\lambda \in I$. Define the [Banach space](/page/Banach%20Space) $D_* := (D,\|\cdot\|_{D_*})$. By hypothesis,
\begin{align*}
H:I \to \mathcal{L}(D_*,\mathcal{H})
\end{align*}
and
\begin{align*}
\psi:I \to D_*
\end{align*}
are differentiable at $\lambda$. Therefore the product map
\begin{align*}
I \to \mathcal{H}, \qquad \mu \mapsto H(\mu)\psi(\mu)
\end{align*}
is differentiable at $\lambda$, with derivative
\begin{align*}
H'(\lambda)\psi(\lambda)+H(\lambda)\psi'(\lambda).
\end{align*}
The right-hand side of the eigenvalue equation is the product of the scalar function $E:I\to\mathbb{R}$ and the vector-valued function $\psi:I\to D_*\subset\mathcal{H}$, so
\begin{align*}
\frac{d}{d\lambda}\bigl(E(\lambda)\psi(\lambda)\bigr)
=
E'(\lambda)\psi(\lambda)+E(\lambda)\psi'(\lambda).
\end{align*}
Differentiating
\begin{align*}
H(\lambda)\psi(\lambda)=E(\lambda)\psi(\lambda)
\end{align*}
as an identity in $\mathcal{H}$ gives
\begin{align*}
H'(\lambda)\psi(\lambda)+H(\lambda)\psi'(\lambda)
=
E'(\lambda)\psi(\lambda)+E(\lambda)\psi'(\lambda).
\end{align*}
[guided]
Fix $\lambda \in I$, and let $D_* := (D,\|\cdot\|_{D_*})$ denote the common domain equipped with the graph norm of the reference operator $H(\lambda_*)$. The reason for introducing $D_*$ is that $H(\lambda)$ is generally unbounded as an operator on $\mathcal{H}$, but by hypothesis it is a bounded operator
\begin{align*}
H(\lambda):D_* \to \mathcal{H}.
\end{align*}
Thus the expression $H(\lambda)\psi(\lambda)$ is a product of a differentiable operator-valued map and a differentiable vector-valued map between Banach spaces.
We verify the product rule directly. For $\mu \neq \lambda$, write
\begin{align*}
\frac{H(\mu)\psi(\mu)-H(\lambda)\psi(\lambda)}{\mu-\lambda}
=
\frac{H(\mu)-H(\lambda)}{\mu-\lambda}\psi(\mu)
+
H(\lambda)\frac{\psi(\mu)-\psi(\lambda)}{\mu-\lambda}.
\end{align*}
Since $\psi:I\to D_*$ is differentiable, $\psi(\mu)\to\psi(\lambda)$ in $D_*$ as $\mu\to\lambda$. Since $H:I\to\mathcal{L}(D_*,\mathcal{H})$ is differentiable in operator norm,
\begin{align*}
\frac{H(\mu)-H(\lambda)}{\mu-\lambda}\to H'(\lambda)
\end{align*}
in $\mathcal{L}(D_*,\mathcal{H})$. Hence the first term converges in $\mathcal{H}$ to $H'(\lambda)\psi(\lambda)$, and the second term converges in $\mathcal{H}$ to $H(\lambda)\psi'(\lambda)$ because $H(\lambda):D_*\to\mathcal{H}$ is bounded. Therefore
\begin{align*}
\frac{d}{d\lambda}\bigl(H(\lambda)\psi(\lambda)\bigr)
=
H'(\lambda)\psi(\lambda)+H(\lambda)\psi'(\lambda).
\end{align*}
The right-hand side of the eigenvalue equation is easier: $E:I\to\mathbb{R}$ is differentiable and $\psi:I\to D_*$ is differentiable, hence also differentiable as an $\mathcal{H}$-valued map because the graph norm dominates the Hilbert norm. The scalar-vector product rule gives
\begin{align*}
\frac{d}{d\lambda}\bigl(E(\lambda)\psi(\lambda)\bigr)
=
E'(\lambda)\psi(\lambda)+E(\lambda)\psi'(\lambda).
\end{align*}
Differentiating the identity
\begin{align*}
H(\lambda)\psi(\lambda)=E(\lambda)\psi(\lambda)
\end{align*}
therefore yields
\begin{align*}
H'(\lambda)\psi(\lambda)+H(\lambda)\psi'(\lambda)
=
E'(\lambda)\psi(\lambda)+E(\lambda)\psi'(\lambda).
\end{align*}
[/guided]
[/step]
[step:Take the inner product with the normalized eigenvector]
Taking the inner product of the differentiated identity with $\psi(\lambda)$ in the second variable gives
\begin{align*}
(H'(\lambda)\psi(\lambda),\psi(\lambda))_{\mathcal{H}}
+
(H(\lambda)\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}
=
E'(\lambda)(\psi(\lambda),\psi(\lambda))_{\mathcal{H}}
+
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}.
\end{align*}
Since $\|\psi(\lambda)\|_{\mathcal{H}}=1$,
\begin{align*}
(\psi(\lambda),\psi(\lambda))_{\mathcal{H}}=1.
\end{align*}
Thus
\begin{align*}
(H'(\lambda)\psi(\lambda),\psi(\lambda))_{\mathcal{H}}
+
(H(\lambda)\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}
=
E'(\lambda)
+
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}.
\end{align*}
[/step]
[step:Use self-adjointness to identify the term containing $\psi'(\lambda)$]
Because $\psi:I\to D_*$ is differentiable, $\psi'(\lambda)\in D$. Since $H(\lambda)$ is self-adjoint on the domain $D$ and both $\psi'(\lambda)$ and $\psi(\lambda)$ belong to $D$,
\begin{align*}
(H(\lambda)\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}
=
(\psi'(\lambda),H(\lambda)\psi(\lambda))_{\mathcal{H}}.
\end{align*}
Using the eigenvalue equation $H(\lambda)\psi(\lambda)=E(\lambda)\psi(\lambda)$ and the fact that $E(\lambda)\in\mathbb{R}$, we get
\begin{align*}
(\psi'(\lambda),H(\lambda)\psi(\lambda))_{\mathcal{H}}
=
(\psi'(\lambda),E(\lambda)\psi(\lambda))_{\mathcal{H}}
=
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}.
\end{align*}
Therefore
\begin{align*}
(H(\lambda)\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}
=
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}.
\end{align*}
[/step]
[step:Cancel the matching eigenvector-derivative terms]
Substituting the identity from the previous step into the inner-product equation gives
\begin{align*}
(H'(\lambda)\psi(\lambda),\psi(\lambda))_{\mathcal{H}}
+
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}
=
E'(\lambda)
+
E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}.
\end{align*}
Subtracting the scalar $E(\lambda)(\psi'(\lambda),\psi(\lambda))_{\mathcal{H}}$ from both sides yields
\begin{align*}
(H'(\lambda)\psi(\lambda),\psi(\lambda))_{\mathcal{H}}
=
E'(\lambda).
\end{align*}
Since $\lambda\in I$ was arbitrary, the identity holds for every $\lambda\in I$, which is the desired formula.
[/step]
