[proofplan] The equations $\partial_{\alpha_j}S=\beta_j$ define $y$ locally by the inverse function theorem because the mixed matrix $S_{y\alpha}$ is invertible. Differentiating these equations with respect to $x$ gives a linear system involving $y'$. Differentiating the Hamilton-Jacobi equation with respect to $\alpha$ gives the same linear system with $\partial_pH$ in place of $y'$, so invertibility forces $y'=\partial_pH$. Differentiating $p=\nabla_yS$ and using the $y$-derivative of the Hamilton-Jacobi equation gives $p'=-\partial_yH$. [/proofplan]

[step:Use the nondegeneracy condition to solve for $y$ locally]Define $F:I\times V\to\mathbb{R}^n$ by \begin{align*} F(x,y):=\nabla_\alpha S(x,y,\alpha_0)-\beta. \end{align*} The hypotheses give $F(x_0,y_0)=0$. The derivative of $F$ with respect to $y$ at $(x_0,y_0)$ is the [linear map](/page/Linear%20Map) represented by $M_0^\top$, because the $j$th component of $F$ is $\partial_{\alpha_j}S-\beta_j$. Since $M_0$ is invertible, $M_0^\top$ is invertible. By the [Inverse Function Theorem](/theorems/51), after shrinking to a neighbourhood of $x_0$, there is an open interval $J\subset I$ containing $x_0$ and a $C^1$ curve $y:J\to V$ with $y(x_0)=y_0$ such that \begin{align*} F(x,y(x))=0 \end{align*} for every $x\in J$. Equivalently, \begin{align*} \partial_{\alpha_j}S(x,y(x),\alpha_0)=\beta_j \end{align*} for every $j=1,\ldots,n$.[/step]

[guided]The system $\nabla_\alpha S(x,y,\alpha_0)=\beta$ is meant to determine the unknown $y$ as a function of $x$. To use the inverse function theorem, we freeze the parameter $\alpha_0$ and define \begin{align*} F(x,y)=\nabla_\alpha S(x,y,\alpha_0)-\beta. \end{align*} At the base point, the equations in the statement say $F(x_0,y_0)=0$. The derivative of $F$ with respect to $y$ has entries \begin{align*} \partial_{y_i}F_j(x_0,y_0)=\partial_{y_i}\partial_{\alpha_j}S(x_0,y_0,\alpha_0). \end{align*} Thus $D_yF(x_0,y_0)$ is represented by $M_0^\top$. Since $M_0$ is invertible, this derivative is an isomorphism. The [Inverse Function Theorem](/theorems/51) therefore solves $F(x,y)=0$ uniquely for $y$ as a $C^1$ function of $x$ near $x_0$. This gives a curve $y:J\to V$ satisfying \begin{align*} \nabla_\alpha S(x,y(x),\alpha_0)=\beta \end{align*} for all $x\in J$.[/guided]

[step:Differentiate the parameter equations to obtain the first Hamilton equation] For $x\in J$, set \begin{align*} p(x):=\nabla_yS(x,y(x),\alpha_0). \end{align*} Differentiate the identity \begin{align*} \nabla_\alpha S(x,y(x),\alpha_0)=\beta \end{align*} with respect to $x$. Since $\beta$ is constant, this gives \begin{align*} S_{x\alpha}(x,y(x),\alpha_0)+S_{y\alpha}(x,y(x),\alpha_0)^\top y'(x)=0. \end{align*} Now differentiate the Hamilton-Jacobi equation \begin{align*} \partial_xS(x,y,\alpha_0)+H(x,y,\nabla_yS(x,y,\alpha_0))=0 \end{align*} with respect to $\alpha$ while holding $(x,y)$ fixed. The chain rule gives \begin{align*} S_{x\alpha}(x,y,\alpha_0)+S_{y\alpha}(x,y,\alpha_0)^\top\partial_pH(x,y,\nabla_yS(x,y,\alpha_0))=0. \end{align*} Evaluating at $y=y(x)$ and using $p(x)=\nabla_yS(x,y(x),\alpha_0)$, we obtain \begin{align*} S_{y\alpha}(x,y(x),\alpha_0)^\top\left(y'(x)-\partial_pH(x,y(x),p(x))\right)=0. \end{align*} After shrinking $J$ if necessary, $S_{y\alpha}(x,y(x),\alpha_0)$ remains invertible by continuity and the invertibility of $M_0$. Hence \begin{align*} y'(x)=\partial_pH(x,y(x),p(x)). \end{align*} [/step]

[step:Differentiate the momentum definition to obtain the second Hamilton equation] Differentiate \begin{align*} p(x)=\nabla_yS(x,y(x),\alpha_0) \end{align*} with respect to $x$. This gives \begin{align*} p'(x)=S_{xy}(x,y(x),\alpha_0)+S_{yy}(x,y(x),\alpha_0)y'(x). \end{align*} Differentiate the Hamilton-Jacobi equation with respect to $y$ while holding $\alpha_0$ fixed: \begin{align*} S_{xy}(x,y,\alpha_0)+S_{yy}(x,y,\alpha_0)\partial_pH(x,y,\nabla_yS(x,y,\alpha_0))+\partial_yH(x,y,\nabla_yS(x,y,\alpha_0))=0. \end{align*} Evaluate this identity at $y=y(x)$ and use the first Hamilton equation $y'(x)=\partial_pH(x,y(x),p(x))$. The previous two displays combine to give \begin{align*} p'(x)=-\partial_yH(x,y(x),p(x)). \end{align*} Together with the first Hamilton equation, this proves that $(y,p)$ solves Hamilton's equations on $J$. [/step]