Sard's theorem proof - Using Implicit Function Theorem to construct a new coordinate representation The following is part of the proof of the Sard's theorem from John Lee's Introduction to Smooth Manifolds. I am struggling to understand the second paragraph from Step 1.
So assuming that $\partial F^1 / \partial x^1(a)\neq 0 $, how do we define new smooth coordinates $(u,v)=(u,v^2,\dots , v^m)$ in some neighborhood $V_a$ of $a$ in $U$ by
$u=F^1, v^2 = x^2 ,\dots ,v^m=x^m?$ I think this is some form of the implicit function theorem, but from the theorem stated in the text, I cannot figure out how we can construct such a coordinate chart. Also, in terms of these coordinates how does F have the coordinate representation
$$F(u,v^2, \dots, v^m) = (u,F^2(u,v),\dots ,F^n(u,v))?$$
These are probably simple applications of the theorem but I am really struggling to understand this formally. I would greatly appreciate some help.



 A: This is an application of the inverse function theorem. Define
$$ \Phi(x^1,\dots,x^m) = (F^1(x^1,\dots,x^m),x^2,\dots,x^m) $$
and denote the coordinates in the codomain by $u,v^2,\dots,v^m$. The differential of $\Phi$ at $\mathbf{a} = (a^1,\dots,a^m)$ is
$$ d\Phi|_{(a^1,\dots,a^m)} = \begin{pmatrix} \frac{\partial F}{\partial x^1}(\mathbf{a}) & \frac{\partial F}{\partial x^2}(\mathbf{a}) & \dots & \frac{\partial F}{\partial x^m}(\mathbf{a}) \\
0 & 1 & \dots & 0 \\
\vdots & \vdots  & \ddots & \vdots \\
0 & 0 & \cdots  & 1\end{pmatrix} $$
and so since $\frac{\partial F}{\partial x^1}(\mathbf{a}) \neq 0$, the differential is invertible at $a$ so you can invert $\Phi$ locally near $a$. Call the inverse
$$G = G(u,v^2,\dots,v^m) = G(u,\mathbf{v}) =  \left(G^1(u,\mathbf{v}), \dots G^m(u,\mathbf{v}) \right). $$ Then
$$ (\Phi \circ G)(u,\mathbf{v}) = 
\left( F^1(G^1(u,\mathbf{v}),\dots,G^m(u,\mathbf{v})), G^2(u,\mathbf{v}),\dots,G^m(u,\mathbf{v}) \right) 
= \\
(u,v_2,\dots,v_m). $$
This implies that
$$ (F \circ G)(u,\mathbf{v}) = \\
\left( F^1(G^1(u,\mathbf{v}), \dots, G^m(u,\mathbf{v})), F^2(G^1(u,\mathbf{v}), \dots, G^m(u,\mathbf{v})),\dots, F^n(G^1(u,\mathbf{v}),\dots,G^n(u,\mathbf{v})) \right) \\
=
\left( u, F^2(G^1(u,\mathbf{v}),\mathbf{v}), \dots F^n(G^1(u,\mathbf{v}),\mathbf{v}) \right).$$
So if we abuse notation and write $F(u,\mathbf{v})$ for $F \circ G$ and similarly for the coordinates of $F$ then we have
$$ F(u,v_1,\dots,v_m) = \left( u, F^2(u,\mathbf{v}), \dots, F^n (u,\mathbf{v}) \right). $$
