[proofplan]
The proof is the chain-rule computation along an integral curve of the Hamiltonian vector field. For each initial point $p$, the velocity of the flow curve $t\mapsto \varphi_t(p)$ is $X_H(\varphi_t(p))$, so differentiating $F(\varphi_t(p))$ gives the Poisson bracket $\{F,H\}$ evaluated along the same curve. Vanishing of the bracket therefore forces the derivative of $F$ along every trajectory to vanish, while conservation along all local trajectories gives the bracket vanishing by evaluating that derivative at time $0$.
[/proofplan]
[step:Differentiate $F$ along each Hamiltonian trajectory]
Fix $p\in M$. Define the time interval
\begin{align*}
I_p:=\{t\in\mathbb R:(t,p)\in D\}.
\end{align*}
Let $J\subset I_p$ be a [connected component](/page/Connected%20Component). The trajectory through $p$ on $J$ is the smooth curve
\begin{align*}
\gamma_p:J&\to M
\end{align*}
\begin{align*}
t&\mapsto \varphi_t(p).
\end{align*}
Since $\varphi$ is the flow of $X_H$, the velocity of this curve is
\begin{align*}
\frac{d\gamma_p}{dt}(t)=X_H(\gamma_p(t))
\end{align*}
for every $t\in J$. Applying the chain rule for the smooth map $F:M\to\mathbb R$ and the smooth curve $\gamma_p:J\to M$ gives
\begin{align*}
\frac{d}{dt}(F\circ\gamma_p)(t)=dF_{\gamma_p(t)}\left(\frac{d\gamma_p}{dt}(t)\right).
\end{align*}
Substituting the flow equation and using the Poisson bracket convention $\{F,H\}=dF(X_H)$, we obtain
\begin{align*}
\frac{d}{dt}F(\varphi_t(p))=\{F,H\}(\varphi_t(p)).
\end{align*}
[guided]
Fix an initial point $p\in M$. Because a Hamiltonian vector field need not be complete, the flow may only be defined for a local interval of times. We therefore define
\begin{align*}
I_p:=\{t\in\mathbb R:(t,p)\in D\}.
\end{align*}
If $J\subset I_p$ is a connected component, then the trajectory through $p$ on this component is the smooth curve
\begin{align*}
\gamma_p:J&\to M
\end{align*}
\begin{align*}
t&\mapsto \varphi_t(p).
\end{align*}
The defining property of the flow of the vector field $X_H$ is that the velocity of this curve at time $t$ is the value of $X_H$ at the current point of the curve:
\begin{align*}
\frac{d\gamma_p}{dt}(t)=X_H(\gamma_p(t)).
\end{align*}
Now apply the chain rule to the smooth function $F:M\to\mathbb R$ and the smooth curve $\gamma_p:J\to M$. The chain rule gives
\begin{align*}
\frac{d}{dt}(F\circ\gamma_p)(t)=dF_{\gamma_p(t)}\left(\frac{d\gamma_p}{dt}(t)\right).
\end{align*}
Replacing the curve velocity by the Hamiltonian vector field gives
\begin{align*}
\frac{d}{dt}(F\circ\gamma_p)(t)=dF_{\gamma_p(t)}(X_H(\gamma_p(t))).
\end{align*}
With the stated Poisson bracket convention, the smooth function $\{F,H\}:M\to\mathbb R$ is defined by
\begin{align*}
\{F,H\}(x)=dF_x(X_H(x))
\end{align*}
for each $x\in M$. Evaluating this identity at $x=\gamma_p(t)=\varphi_t(p)$ yields
\begin{align*}
\frac{d}{dt}F(\varphi_t(p))=\{F,H\}(\varphi_t(p)).
\end{align*}
This is the central computation: conservation of $F$ along the flow is exactly the assertion that the derivative on the left vanishes along every trajectory.
[/guided]
[/step]
[step:Use vanishing of the Poisson bracket to prove conservation]
Assume that $\{F,H\}=0$ on $M$. For every $p\in M$, every connected component $J\subset I_p$, and every $t\in J$, the identity from the previous step gives
\begin{align*}
\frac{d}{dt}F(\varphi_t(p))=0.
\end{align*}
Since $J$ is an interval in $\mathbb R$, the one-variable [mean value theorem](/theorems/186) implies that the smooth map
\begin{align*}
J&\to\mathbb R
\end{align*}
\begin{align*}
t&\mapsto F(\varphi_t(p))
\end{align*}
is constant. Hence $F$ is conserved along the Hamiltonian flow of $H$.
[/step]
[step:Use conservation on local trajectories to force the bracket to vanish]
Conversely, assume that $F$ is conserved along the Hamiltonian flow of $H$. Fix $p\in M$. Since $\varphi$ is a flow, $(0,p)\in D$ and $\varphi_0(p)=p$. Let $J\subset I_p$ be the connected component containing $0$. By conservation, the smooth map
\begin{align*}
J&\to\mathbb R
\end{align*}
\begin{align*}
t&\mapsto F(\varphi_t(p))
\end{align*}
is constant, so its derivative at $t=0$ is zero. Using the differentiation identity from the first step at $t=0$, we get
\begin{align*}
0=\frac{d}{dt}\bigg|_{t=0}F(\varphi_t(p))=\{F,H\}(\varphi_0(p))=\{F,H\}(p).
\end{align*}
Because $p\in M$ was arbitrary, $\{F,H\}=0$ on $M$. This proves the converse implication and completes the proof.
[/step]
