[proofplan]
We differentiate the expectation value $t\mapsto (A\psi(t),\psi(t))_H$ using the product rule for the Hilbert-space [inner product](/page/Inner%20Product). The explicit domain hypothesis and derivative identity $(A\psi)'(t)=A\psi'(t)$ permit differentiating through the possibly unbounded operator $A$, and the Schrödinger equation then converts time derivatives into applications of $\mathcal H$. Finally, self-adjointness of $\mathcal H$ moves $\mathcal H$ from the second inner-product slot to the first, producing the commutator $\mathcal H A-A\mathcal H$.
[/proofplan]
[step:Verify that all operator products in the commutator are defined]
Let $\mathcal D \subset D(A) \cap D(\mathcal H)$ denote the common invariant domain from the theorem statement. Fix $t\in I$. Since $\psi(t)\in\mathcal D$, the assumptions $\mathcal H(\mathcal D)\subset D(A)$ and $A(\mathcal D)\subset D(\mathcal H)$ imply
\begin{align*}
\mathcal H\psi(t)\in D(A)
\end{align*}
and
\begin{align*}
A\psi(t)\in D(\mathcal H).
\end{align*}
Therefore $A\mathcal H\psi(t)$ and $\mathcal H A\psi(t)$ are both defined as elements of $H$. Thus $(\mathcal H A-A\mathcal H)\psi(t)$ is a well-defined vector in $H$.
[/step]
[step:Differentiate the expectation value and insert the Schrödinger equation]
Define the expectation map $E:I\to\mathbb C$ by
\begin{align*}
E(s)=(A\psi(s),\psi(s))_H.
\end{align*}
The maps $s\mapsto A\psi(s)$ and $s\mapsto\psi(s)$ are strongly differentiable as maps from $I$ to $H$, so applying the product rule to the continuous sesquilinear Hilbert-space inner product gives
\begin{align*}
E'(t)=((A\psi)'(t),\psi(t))_H+(A\psi(t),\psi'(t))_H.
\end{align*}
Using the stated derivative identity $(A\psi)'(t)=A\psi'(t)$ and the strong Schrödinger equation $\psi'(t)=-i\mathcal H\psi(t)$, and using linearity of the inner product in the first argument and conjugate-linearity in the second argument, we obtain
\begin{align*}
E'(t)=(-iA\mathcal H\psi(t),\psi(t))_H+(A\psi(t),-i\mathcal H\psi(t))_H.
\end{align*}
Since the second slot is conjugate-linear, $(A\psi(t),-i\mathcal H\psi(t))_H=i(A\psi(t),\mathcal H\psi(t))_H$. Hence
\begin{align*}
E'(t)=-i(A\mathcal H\psi(t),\psi(t))_H+i(A\psi(t),\mathcal H\psi(t))_H.
\end{align*}
[guided]
We want to differentiate the scalar function measuring the expectation of $A$ in the state $\psi(t)$. Define the expectation map $E:I\to\mathbb C$ by
\begin{align*}
E(s)=(A\psi(s),\psi(s))_H.
\end{align*}
The product rule applies because both maps $s\mapsto A\psi(s)$ and $s\mapsto\psi(s)$ are strongly differentiable as $H$-valued maps and the Hilbert-space inner product is a continuous sesquilinear map from $H\times H$ to $\mathbb C$. Therefore
\begin{align*}
E'(t)=((A\psi)'(t),\psi(t))_H+(A\psi(t),\psi'(t))_H.
\end{align*}
The derivative identity hypothesis is used exactly here: the assumption $(A\psi)'(t)=A\psi'(t)$ makes the formal operation of differentiating through the possibly unbounded operator $A$ legitimate. Differentiability of $s\mapsto A\psi(s)$ alone would not imply this identity for an unbounded operator. Since $\psi$ solves the Schrödinger equation, $\psi'(t)=-i\mathcal H\psi(t)$. Substituting this into both derivative terms gives
\begin{align*}
E'(t)=(A(-i\mathcal H\psi(t)),\psi(t))_H+(A\psi(t),-i\mathcal H\psi(t))_H.
\end{align*}
Because $A$ is linear, the first term is $(-iA\mathcal H\psi(t),\psi(t))_H$. Since the Hilbert-space inner product is linear in the first argument and conjugate-linear in the second argument, the scalar $-i$ leaves the first slot as $-i$ but leaves the second slot as its conjugate $i$. Thus
\begin{align*}
E'(t)=-i(A\mathcal H\psi(t),\psi(t))_H+i(A\psi(t),\mathcal H\psi(t))_H.
\end{align*}
This is the differentiated expectation value before using self-adjointness.
[/guided]
[/step]
[step:Move $\mathcal H$ to the first inner-product slot and identify the commutator]
By the defining symmetry property of the self-adjoint operator $\mathcal H$, since $A\psi(t)\in D(\mathcal H)$ and $\psi(t)\in D(\mathcal H)$, we have
\begin{align*}
(A\psi(t),\mathcal H\psi(t))_H=(\mathcal H A\psi(t),\psi(t))_H.
\end{align*}
Substituting this into the formula for $E'(t)$ yields
\begin{align*}
E'(t)=-i(A\mathcal H\psi(t),\psi(t))_H+i(\mathcal H A\psi(t),\psi(t))_H.
\end{align*}
Factoring out $i$ gives
\begin{align*}
E'(t)=i((\mathcal H A-A\mathcal H)\psi(t),\psi(t))_H.
\end{align*}
Since $t\in I$ was arbitrary, the identity holds for every $t\in I$.
[/step]
