[proofplan] The Hamiltonian is the Legendre transform of $L$ in the velocity variable. We differentiate the defining expression $H=p\cdot v-L(x,y,v)$, remembering that $v=v(x,y,p)$ depends on all variables. The terms containing derivatives of $v$ cancel because the inverse Legendre relation says $p=\partial_v L(x,y,v)$. The remaining coefficients give the three derivative identities, and the recovery formula is just the defining equation rearranged. [/proofplan]

[step:Differentiate the Hamiltonian while tracking the inverse velocity]Fix $(x,y,p)\in W$ and write \begin{align*} v:=v(x,y,p). \end{align*} The defining relation for the inverse velocity map is \begin{align*} p=\partial_v L(x,y,v). \end{align*} Because $L$ is $C^2$ and $v:W\to\mathbb{R}^n$ is $C^1$, the Hamiltonian \begin{align*} H(x,y,p)=p\cdot v(x,y,p)-L(x,y,v(x,y,p)) \end{align*} is $C^1$ on $W$. Let $(\dot x,\dot y,\dot p)\in\mathbb{R}\times\mathbb{R}^n\times\mathbb{R}^n$ be a tangent vector. Applying the chain rule to $H$ at $(x,y,p)$ gives \begin{align*} dH(x,y,p)[\dot x,\dot y,\dot p]=\dot p\cdot v+p\cdot dv[\dot x,\dot y,\dot p]-\partial_xL(x,y,v)\dot x-\partial_yL(x,y,v)\cdot\dot y-\partial_vL(x,y,v)\cdot dv[\dot x,\dot y,\dot p]. \end{align*} Here $dv[\dot x,\dot y,\dot p]\in\mathbb{R}^n$ denotes the directional derivative of the inverse velocity map at $(x,y,p)$ in the chosen direction. Since $p=\partial_vL(x,y,v)$, the two terms involving $dv[\dot x,\dot y,\dot p]$ cancel. Therefore \begin{align*} dH(x,y,p)[\dot x,\dot y,\dot p]=\dot p\cdot v-\partial_xL(x,y,v)\dot x-\partial_yL(x,y,v)\cdot\dot y. \end{align*}[/step]

[guided]The only delicate point is that $v$ is not an independent variable after the Legendre transform. It is the function $v(x,y,p)$ selected by the equation \begin{align*} p=\partial_vL(x,y,v(x,y,p)). \end{align*} So, when differentiating $H$, every change in $(x,y,p)$ also changes $v$. Take a tangent direction $(\dot x,\dot y,\dot p)$. The product rule applied to $p\cdot v(x,y,p)$ gives \begin{align*} \dot p\cdot v+p\cdot dv[\dot x,\dot y,\dot p]. \end{align*} The chain rule applied to $L(x,y,v(x,y,p))$ gives \begin{align*} \partial_xL(x,y,v)\dot x+\partial_yL(x,y,v)\cdot\dot y+\partial_vL(x,y,v)\cdot dv[\dot x,\dot y,\dot p]. \end{align*} Subtracting the second expression from the first, as required by the definition of $H$, gives \begin{align*} dH(x,y,p)[\dot x,\dot y,\dot p]=\dot p\cdot v+p\cdot dv[\dot x,\dot y,\dot p]-\partial_xL(x,y,v)\dot x-\partial_yL(x,y,v)\cdot\dot y-\partial_vL(x,y,v)\cdot dv[\dot x,\dot y,\dot p]. \end{align*} Now use the inverse Legendre relation. Because $p=\partial_vL(x,y,v)$, the term \begin{align*} p\cdot dv[\dot x,\dot y,\dot p] \end{align*} is exactly the same scalar as \begin{align*} \partial_vL(x,y,v)\cdot dv[\dot x,\dot y,\dot p]. \end{align*} They occur with opposite signs, so they cancel. What remains is \begin{align*} dH(x,y,p)[\dot x,\dot y,\dot p]=\dot p\cdot v-\partial_xL(x,y,v)\dot x-\partial_yL(x,y,v)\cdot\dot y. \end{align*}[/guided]

[step:Read off the partial derivative identities] The formula for the differential holds for every tangent vector. First take $\dot x=0$, $\dot y=0$, and arbitrary $\dot p\in\mathbb{R}^n$. Then \begin{align*} dH(x,y,p)[0,0,\dot p]=\dot p\cdot v. \end{align*} By the defining property of the gradient with respect to $p$, this means \begin{align*} \partial_pH(x,y,p)=v(x,y,p). \end{align*} Next take $\dot x=0$, $\dot p=0$, and arbitrary $\dot y\in\mathbb{R}^n$. The differential formula gives \begin{align*} dH(x,y,p)[0,\dot y,0]=-\partial_yL(x,y,v)\cdot\dot y. \end{align*} Therefore \begin{align*} \partial_yH(x,y,p)=-\partial_yL(x,y,v(x,y,p)). \end{align*} Finally take $\dot y=0$, $\dot p=0$, and arbitrary $\dot x\in\mathbb{R}$. Then \begin{align*} dH(x,y,p)[\dot x,0,0]=-\partial_xL(x,y,v)\dot x. \end{align*} Thus \begin{align*} \partial_xH(x,y,p)=-\partial_xL(x,y,v(x,y,p)). \end{align*} [/step]

[step:Recover the Lagrangian from the Hamiltonian] Let $(x,y,v_0)\in\Omega$ and set \begin{align*} p:=\partial_vL(x,y,v_0). \end{align*} Then $p=\Lambda_{x,y}(v_0)$, so $(x,y,p)\in W$. Since $v(x,y,p)$ is the inverse image of $p$ under $\Lambda_{x,y}$, we have \begin{align*} v(x,y,p)=v_0. \end{align*} The definition of $H$ gives \begin{align*} H(x,y,p)=p\cdot v_0-L(x,y,v_0). \end{align*} Rearranging this equality yields \begin{align*} L(x,y,v_0)=p\cdot v_0-H(x,y,p). \end{align*} [/step]