I'm currently proving that three different definitions of a submanifold of $\mathbb{R}^{n+m}$ are equivalent, and I've mostly done it, but there's one implication that I'm struggling with.
For $M \subseteq \mathbb{R}^{n+m}$,
Definition 1: $\forall x_0 \in M, \exists U \subseteq \mathbb{R}^{n+m}$ an open neighbourhood of $x_0$, an open subset $W \subseteq \mathbb{R}^n$ and a $C^\infty$-map $\psi: W \longrightarrow U$ such that $\psi$ is a homeomorphism of $W$ onto $\psi(W) = M \cap U$ and $D\psi(w)$ is injective for all $w \in W$.
Definition 2: $\forall x_0 \in M, \exists U \subseteq \mathbb{R}^{n+m}$ an open neighbourhood of $x_0$ and a $C^\infty$-map $f: U \longrightarrow \mathbb{R}^m$ whose Jacobian $Df(x)$ has rank $m$ for all $x \in U$ such that $U \cap M = \{x \in U \,|\, f(x) = 0\} = f^{-1}(\{0\})$.
I need to prove that definition 1 implies definition 2.
I ran out of time when I posted this before, but my ideas thus far have amounted to:
Define $g: W\times \mathbb{R}^m \rightarrow \mathbb{R}^{m+n}, \; (w,y) \longmapsto \left(\psi(w),y\right).$ Then $g$ is locally invertible, and so for some $V \subseteq \mathbb{R}^{n+m}$ and U' \subseteq U, $g$ is a diffeomorphism from $V$ onto V', as g|_V : V \rightarrow U' is invertible.
U' \xrightarrow{(g|_V)^{-1}} V \xrightarrow{pr} \mathbb{R}^m, where $pr$ is the projection from $V$ to $\mathbb{R}^m$, so define:
f: U' \longrightarrow \mathbb{R}^m, \; x \longmapsto \left(pr \circ (g|_V)^{-1} \right) (x).
I don't know whether I'm barking up the wrong tree here, or quite how to show that it satisfies the requirements $\ldots$