[proofplan]
We verify each of the five properties of the Poisson bracket $\{F, G\} = \sum_{i,j} \frac{\partial F}{\partial x_i} J_{ij} \frac{\partial G}{\partial x_j}$, where $J = \begin{pmatrix} 0 & I_n \\ -I_n & 0 \end{pmatrix}$ is the standard symplectic matrix and $x = (q_1, \ldots, q_n, p_1, \ldots, p_n)$. Bilinearity and antisymmetry follow from linearity of partial derivatives and the antisymmetry $J^\top = -J$. The Leibniz rule reduces to the product rule for partial derivatives. The Jacobi identity is verified by direct computation of the triple bracket. The canonical relations are checked by evaluating brackets of the coordinate functions.
[/proofplan]
[step:Verify bilinearity from the linearity of partial differentiation]
Let $F, G, H: \mathbb{R}^{2n} \to \mathbb{R}$ be smooth functions and let $\alpha, \beta \in \mathbb{R}$. The Poisson bracket is
\begin{align*}
\{F, G\} = \sum_{i,j=1}^{2n} \frac{\partial F}{\partial x_i} J_{ij} \frac{\partial G}{\partial x_j} = \left(\nabla F\right)^\top J\, \nabla G,
\end{align*}
where $\nabla F = \left(\frac{\partial F}{\partial x_1}, \ldots, \frac{\partial F}{\partial x_{2n}}\right)^\top$. For linearity in the second argument:
\begin{align*}
\{F, \alpha G + \beta H\} &= (\nabla F)^\top J\, \nabla(\alpha G + \beta H) \\
&= (\nabla F)^\top J\, (\alpha\, \nabla G + \beta\, \nabla H) \\
&= \alpha\, (\nabla F)^\top J\, \nabla G + \beta\, (\nabla F)^\top J\, \nabla H \\
&= \alpha\, \{F, G\} + \beta\, \{F, H\},
\end{align*}
where we used the linearity of the gradient operator and the linearity of matrix multiplication. Linearity in the first argument follows by the same reasoning applied to $\nabla(\alpha F + \beta G)$.
[/step]
[step:Verify antisymmetry from $J^\top = -J$]
Since $J$ is a $2n \times 2n$ matrix satisfying $J^\top = -J$ (i.e., $J$ is skew-symmetric), we have for any smooth $F, G: \mathbb{R}^{2n} \to \mathbb{R}$:
\begin{align*}
\{G, F\} &= (\nabla G)^\top J\, \nabla F \\
&= \left((\nabla G)^\top J\, \nabla F\right)^\top \qquad \text{(a scalar equals its own transpose)} \\
&= (\nabla F)^\top J^\top \nabla G \\
&= (\nabla F)^\top (-J)\, \nabla G \\
&= -(\nabla F)^\top J\, \nabla G \\
&= -\{F, G\}.
\end{align*}
Therefore $\{F, G\} = -\{G, F\}$.
[/step]
[step:Verify the Leibniz rule from the product rule for partial derivatives]
Let $F, G, H: \mathbb{R}^{2n} \to \mathbb{R}$ be smooth. We compute $\{F, GH\}$ using the definition:
\begin{align*}
\{F, GH\} &= \sum_{i,j=1}^{2n} \frac{\partial F}{\partial x_i} J_{ij} \frac{\partial(GH)}{\partial x_j}.
\end{align*}
Applying the product rule for partial derivatives, $\frac{\partial(GH)}{\partial x_j} = G\, \frac{\partial H}{\partial x_j} + H\, \frac{\partial G}{\partial x_j}$, and substituting:
\begin{align*}
\{F, GH\} &= \sum_{i,j} \frac{\partial F}{\partial x_i} J_{ij} \left( G\, \frac{\partial H}{\partial x_j} + H\, \frac{\partial G}{\partial x_j} \right) \\
&= G \sum_{i,j} \frac{\partial F}{\partial x_i} J_{ij} \frac{\partial H}{\partial x_j} + H \sum_{i,j} \frac{\partial F}{\partial x_i} J_{ij} \frac{\partial G}{\partial x_j} \\
&= G\, \{F, H\} + H\, \{F, G\}.
\end{align*}
(In passing $G$ and $H$ through the sums, we used that $G$ does not depend on the dummy indices $i, j$ in the first term, and similarly for $H$ in the second.)
[/step]
[step:Verify the Jacobi identity by direct computation]
We must show that for all smooth $F, G, H: \mathbb{R}^{2n} \to \mathbb{R}$,
\begin{align*}
\{F, \{G, H\}\} + \{G, \{H, F\}\} + \{H, \{F, G\}\} = 0.
\end{align*}
In canonical coordinates $x = (q_1, \ldots, q_n, p_1, \ldots, p_n)$, the Poisson bracket takes the form
\begin{align*}
\{F, G\} = \sum_{k=1}^n \left( \frac{\partial F}{\partial q_k} \frac{\partial G}{\partial p_k} - \frac{\partial F}{\partial p_k} \frac{\partial G}{\partial q_k} \right).
\end{align*}
We compute $\{F, \{G, H\}\}$. By the chain rule,
\begin{align*}
\frac{\partial}{\partial q_k} \{G, H\} &= \sum_{l=1}^n \left( \frac{\partial^2 G}{\partial q_k \partial q_l} \frac{\partial H}{\partial p_l} + \frac{\partial G}{\partial q_l} \frac{\partial^2 H}{\partial q_k \partial p_l} - \frac{\partial^2 G}{\partial q_k \partial p_l} \frac{\partial H}{\partial q_l} - \frac{\partial G}{\partial p_l} \frac{\partial^2 H}{\partial q_k \partial q_l} \right),
\end{align*}
with an analogous expression for $\frac{\partial}{\partial p_k} \{G, H\}$.
When we form $\{F, \{G, H\}\}$ and expand, every term involves one second-order derivative and two first-order derivatives (one from each of the three functions $F$, $G$, $H$). In the cyclic sum $\{F, \{G, H\}\} + \{G, \{H, F\}\} + \{H, \{F, G\}\}$, each term involving a second derivative of $F$ appears twice with opposite signs: once from the expansion of $\{G, \{H, F\}\}$ (where $F$ is differentiated twice inside the inner bracket and then paired with a first derivative of $G$) and once from $\{H, \{F, G\}\}$ (where $F$ is differentiated twice inside the inner bracket and paired with a first derivative of $H$, but the outer bracket reverses the sign).
More explicitly, a typical second-derivative-of-$F$ term in $\{G, \{H, F\}\}$ has the form
\begin{align*}
\frac{\partial G}{\partial q_k} \frac{\partial H}{\partial q_l} \frac{\partial^2 F}{\partial p_k \partial p_l},
\end{align*}
and the corresponding term in $\{H, \{F, G\}\}$ is
\begin{align*}
-\frac{\partial H}{\partial q_l} \frac{\partial G}{\partial q_k} \frac{\partial^2 F}{\partial p_l \partial p_k}.
\end{align*}
Since $\frac{\partial^2 F}{\partial p_k \partial p_l} = \frac{\partial^2 F}{\partial p_l \partial p_k}$ (by smoothness of $F$), these cancel. By symmetry of the argument, all second-derivative terms from $G$ and $H$ cancel in the same way. Since every term in the cyclic sum involves exactly one second derivative, and all such terms cancel pairwise, the entire cyclic sum vanishes.
[/step]
[step:Verify the canonical Poisson bracket relations]
We compute the brackets of the coordinate functions $q_i$ and $p_j$ directly. Recall that $\frac{\partial q_i}{\partial q_k} = \delta_{ik}$, $\frac{\partial q_i}{\partial p_k} = 0$, $\frac{\partial p_j}{\partial q_k} = 0$, and $\frac{\partial p_j}{\partial p_k} = \delta_{jk}$.
**Bracket $\{q_i, q_j\}$:**
\begin{align*}
\{q_i, q_j\} = \sum_{k=1}^n \left( \frac{\partial q_i}{\partial q_k} \frac{\partial q_j}{\partial p_k} - \frac{\partial q_i}{\partial p_k} \frac{\partial q_j}{\partial q_k} \right) = \sum_{k=1}^n \left( \delta_{ik} \cdot 0 - 0 \cdot \delta_{jk} \right) = 0.
\end{align*}
**Bracket $\{p_i, p_j\}$:**
\begin{align*}
\{p_i, p_j\} = \sum_{k=1}^n \left( \frac{\partial p_i}{\partial q_k} \frac{\partial p_j}{\partial p_k} - \frac{\partial p_i}{\partial p_k} \frac{\partial p_j}{\partial q_k} \right) = \sum_{k=1}^n \left( 0 \cdot \delta_{jk} - \delta_{ik} \cdot 0 \right) = 0.
\end{align*}
**Bracket $\{q_i, p_j\}$:**
\begin{align*}
\{q_i, p_j\} = \sum_{k=1}^n \left( \frac{\partial q_i}{\partial q_k} \frac{\partial p_j}{\partial p_k} - \frac{\partial q_i}{\partial p_k} \frac{\partial p_j}{\partial q_k} \right) = \sum_{k=1}^n \left( \delta_{ik} \cdot \delta_{jk} - 0 \cdot 0 \right) = \delta_{ij}.
\end{align*}
These are the canonical relations: $\{q_i, q_j\} = 0$, $\{p_i, p_j\} = 0$, and $\{q_i, p_j\} = \delta_{ij}$.
[/step]
