I will use the following notations for tuples: $\mathbb R^{n+m} \ni (x, y) = (x_1, \dots, x_n, y_1, \dots, y_m)$. Furthermore, let $\mathbf f : \Omega \subset \mathbb{R}^{n + m} \rightarrow \mathbb{R}^m$ be of class $\mathcal C^1$ on $\Omega$, and write $$\mathbf f'(x, y) = (\mathbf f_x'(x, y), \mathbf f_y'(x, y)) \in \mathbb{R}^{m \times (n + m)},$$ where $\mathbf f_x'(x, y) = (D_jf_i(x, y))_{1 \leq i \leq m, 1 \leq j \leq n} \in \mathbb{R}^{m \times n}$ and $\mathbf f_y'(x, y) = (D_{n + j}f_i(x, y))_{1 \leq i, j \leq m} \in \mathbb{R}^{m \times m}$.
Theorem (implicit function). Let $\mathbf f : \Omega \subset \mathbb{R}^{n + m} \rightarrow \mathbb{R}^m$ be of class $\mathcal C^1$ on $\Omega$ and let $(a, b) \in \Omega$ such that $\mathbf f(a, b) = 0$. If $\det \mathbf f_y'(a, b) \neq 0$, then there exists an open neighborhood $A$ of $a$ in $\mathbb{R}^n$, and an open neighborhood $B$ of $b$ in $\mathbb{R}^m$, with $A \times B \subset \Omega$, and a unique $\mathcal C^1$-function $\mathbf g : A \rightarrow B$ such that $\mathbf f(x, \mathbf g(x)) = 0$ for all $x \in A$.
Definition ($k$-dimensional submanifold). A set $M \subset \mathbb{R}^n$ is called a $k$-dimensional submanifold of $\mathbb{R}^n$ if for all $x_0 \in M$, there exists an open neighborhood $\Omega$ of $x_0 \in \mathbb{R}^n$ and a $\mathcal C^1$-function $\mathbf f : \Omega \subset \mathbb{R}^n \rightarrow \mathbb{R}^{n - k}$ such that $$M \cap \Omega = \mathbf f^{-1}(\{0\}) \hspace{10pt} \mbox{and} \hspace{10pt} \mbox{rank } D\mathbf f(x) = n - k \mbox{ for all } x \in M \cap \Omega.$$
What I want to prove is this:
Proposition. The following are equivalent:
(a) $M$ is a $k$-dimensional submanifold of $\mathbb{R}^n$;
(b) For each $x_0 \in M$, write $x_0 = (y_0, z_0)$ with $y_0 \in \mathbb{R}^k$, $z_0 \in \mathbb{R}^{n - k}$, there exists an open neighborhood $U$ of $y_0$ in $\mathbb{R}^k$, an open neighborhood $V$ of $z_0 \in \mathbb{R}^{n - k}$, and a $\mathcal C^1$-function $\mathbf g : U \rightarrow V$ with $\mathbf g(y_0) = z_0$ such that $$M\cap(U \times V) = \{(y_0, \mathbf g(y_0)) : y_0 \in U\}.$$
I can do the proof from (b) to (a):
Define $\Omega = U \times V$, $\mathbf f : \Omega \rightarrow \mathbb{R}^{n - k}$ by $$\mathbf f(y, z) = z - \mathbf g(y).$$ Then $\mathbf f$ is a $ \mathcal C^1$-function, $M \cap \Omega = M \cap (U \times V) = \{(y_0, \mathbf g(y_0)) : y_0 \in U\} = \mathbf f^{-1}(\{0\})$ and $$D\mathbf f(x_0) = D\mathbf f(y_0, z_0) = (-D\mathbf g(y_0), I_{n - k})$$ which is of rank $n - k$ obviously.
There is a little problem when I do the proof from (a) to (b):
By the definition of $k$-dimensional submanifold, for all $x_0 = (y_0, z_0) \in M$, there exists $\Omega$ of $x_0$, and a $\mathcal C^1$-function $\mathbf f : \Omega \rightarrow \mathbb{R}^{n - k}$ such that $$M \cap \Omega = \mathbf f^{-1}(\{0\}) \hspace{10pt} \mbox{and} \hspace{10pt} \mbox{rank } D\mathbf f(x) = n - k \mbox{ for all } x \in M \cap \Omega.$$ Since $x_0 \in M \cap \Omega$, $\mathbf f(x_0) = \mathbf f(y_0, z_0) = 0$ and since rank $D\mathbf f(x) = n - k$, $\det \mathbf f_z'(y_0, z_0) \neq 0$. Hence by the implicit function theorem, there exists an open neighborhood $U$ of $y_0$, an open neighborhood $V$ of $z_0$ and a $\mathcal C^1$-function $\mathbf g : U \rightarrow V$ such that $\mathbf f(y_0, \mathbf g(y_0)) = 0$ for all $y \in U$.
The problem is that although I know that $\mathbf f(x_0) = \mathbf f(y_0, z_0) = \mathbf f(y_0, \mathbf g(y_0)) = 0$, can I conclude $x_0 = (y_0, \mathbf g(y_0))$ and hence $z_0 = \mathbf g(y_0)$? Does $\mathbf g$ need to be injective?
