[proofplan]
We prove that the quantity $H(x) = y'(x) \frac{\partial L}{\partial p}(y(x), y'(x)) - L(y(x), y'(x))$ is constant along solutions of the Euler--Lagrange equation when $L$ has no explicit $x$-dependence. The argument is a direct computation: differentiate $H$ with respect to $x$ using the product rule and the chain rule, exploit the absence of $\frac{\partial L}{\partial x}$ to simplify $\frac{dL}{dx}$, and observe that the remaining terms cancel exactly by virtue of the Euler--Lagrange equation.
[/proofplan]
[step:Define the Beltrami function $H$ and compute $\frac{dH}{dx}$ via the product rule]
Define the function
\begin{align*}
H: [a,b] &\to \mathbb{R} \\
x &\mapsto y'(x) \frac{\partial L}{\partial p}(y(x), y'(x)) - L(y(x), y'(x)).
\end{align*}
Since $y \in C^2([a,b], \mathbb{R})$ and $L \in C^2(\mathbb{R} \times \mathbb{R})$, the function $H$ is $C^1$ on $[a,b]$. Differentiating $H$ with respect to $x$ using the product rule on the first term:
\begin{align*}
\frac{dH}{dx} &= y''(x) \frac{\partial L}{\partial p}(y, y') + y'(x) \frac{d}{dx}\!\left[\frac{\partial L}{\partial p}(y, y')\right] - \frac{d}{dx}\!\left[L(y, y')\right].
\end{align*}
[/step]
[step:Compute $\frac{dL}{dx}$ using the chain rule and the hypothesis that $L$ is independent of $x$]
Since $L = L(u, p)$ has no explicit dependence on $x$, the total derivative $\frac{d}{dx} L(y(x), y'(x))$ is computed purely through the chain rule in the arguments $u = y(x)$ and $p = y'(x)$:
\begin{align*}
\frac{d}{dx} L(y, y') &= \frac{\partial L}{\partial u}(y, y') \cdot y'(x) + \frac{\partial L}{\partial p}(y, y') \cdot y''(x).
\end{align*}
If $L$ had an explicit $x$-dependence, there would be an additional term $\frac{\partial L}{\partial x}(x, y, y')$; its absence is the content of the autonomy hypothesis.
[guided]
The key point is that $L$ is a function of two variables $(u, p)$, not three. When we evaluate $L$ along the curve $y$, we substitute $u = y(x)$ and $p = y'(x)$, so $L(y(x), y'(x))$ depends on $x$ only implicitly through $y$ and $y'$. The chain rule gives
\begin{align*}
\frac{d}{dx} L(y, y') &= \frac{\partial L}{\partial u} \cdot \frac{du}{dx} + \frac{\partial L}{\partial p} \cdot \frac{dp}{dx} = \frac{\partial L}{\partial u} \cdot y' + \frac{\partial L}{\partial p} \cdot y''.
\end{align*}
For a non-autonomous Lagrangian $L(x, u, p)$, this computation would yield
\begin{align*}
\frac{d}{dx} L(x, y, y') &= \frac{\partial L}{\partial x} + \frac{\partial L}{\partial u} \cdot y' + \frac{\partial L}{\partial p} \cdot y'',
\end{align*}
and the extra term $\frac{\partial L}{\partial x}$ would prevent the cancellation in the next step. This is why the Beltrami identity is specific to autonomous Lagrangians.
[/guided]
[/step]
[step:Substitute into $\frac{dH}{dx}$ and cancel using the Euler--Lagrange equation]
Substituting the expression for $\frac{dL}{dx}$ into $\frac{dH}{dx}$:
\begin{align*}
\frac{dH}{dx} &= y'' \frac{\partial L}{\partial p} + y' \frac{d}{dx}\!\left[\frac{\partial L}{\partial p}\right] - \frac{\partial L}{\partial u} \cdot y' - \frac{\partial L}{\partial p} \cdot y''.
\end{align*}
The terms $y'' \frac{\partial L}{\partial p}$ and $-\frac{\partial L}{\partial p} \cdot y''$ cancel, leaving
\begin{align*}
\frac{dH}{dx} &= y'(x) \left[\frac{d}{dx}\frac{\partial L}{\partial p}(y, y') - \frac{\partial L}{\partial u}(y, y')\right].
\end{align*}
By hypothesis, $y$ is a solution of the [Euler--Lagrange equation](/theorems/3504): $\frac{\partial L}{\partial u}(y, y') - \frac{d}{dx}\frac{\partial L}{\partial p}(y, y') = 0$, i.e., the bracket $\frac{d}{dx}\frac{\partial L}{\partial p} - \frac{\partial L}{\partial u} = 0$. Therefore
\begin{align*}
\frac{dH}{dx} &= y'(x) \cdot 0 = 0
\end{align*}
for all $x \in [a,b]$. Since $\frac{dH}{dx} = 0$ identically, $H$ is constant on $[a,b]$, i.e., $y'(x) \frac{\partial L}{\partial p}(y, y') - L(y, y') = c$ for some $c \in \mathbb{R}$.
[guided]
Let us track the cancellation in detail. Starting from
\begin{align*}
\frac{dH}{dx} &= \underbrace{y'' L_p}_{(1)} + \underbrace{y' \frac{d}{dx} L_p}_{(2)} - \underbrace{L_u y'}_{(3)} - \underbrace{L_p y''}_{(4)},
\end{align*}
terms (1) and (4) cancel immediately (they are the same product $y'' L_p$ with opposite signs). This cancellation is purely algebraic and does not use the Euler--Lagrange equation.
The remaining terms are
\begin{align*}
\frac{dH}{dx} &= y' \frac{d}{dx} L_p - L_u y' = y'\!\left(\frac{d}{dx} L_p - L_u\right).
\end{align*}
The factor in brackets is $\frac{d}{dx} L_p - L_u$, which is exactly the negative of the Euler--Lagrange expression $L_u - \frac{d}{dx} L_p$. By hypothesis, $y$ satisfies $L_u - \frac{d}{dx} L_p = 0$, so the bracket vanishes, giving $\frac{dH}{dx} = 0$.
The structure of this argument reveals why the result works: the product rule creates a pair of $y'' L_p$ terms that cancel algebraically, and the Euler--Lagrange equation kills the remaining factor. The autonomy of $L$ was used in the previous step to ensure that $\frac{dL}{dx} = L_u y' + L_p y''$ has no $\frac{\partial L}{\partial x}$ term; if it did, $\frac{dH}{dx}$ would equal $-\frac{\partial L}{\partial x}$ rather than zero, and $H$ would not be conserved.
[/guided]
[/step]
