Different definitions for submanifolds

I'm trying to better understand the concept of differentiable submanifold. However, it looks like many different definitions are adopted by various authors and so I'm trying to keep myself in sync by proving them equivalent. Now I'm stuck with the following two.

Let $M$ denote a $n$-differentiable manifold and let $M' \subset M$: consider $M'$ equipped with the subspace topology. Also let $n' < n$ be an integer.

I) We say that $M'$ is a $n'$-submanifold of $M$ if it is locally a slice of coordinate system, i.e. for all $p'\in M'$ there exists a coordinate system $(U, x^1 \ldots x^n)$ for $M$ s.t.

$$U \cap M'=\{ p \in M\mid x^{n'+1}(p)=\ldots=x^{n}(p)=0\}.$$

If this is the case $(U \cap M', x^1 \ldots x^{n'})$ is a local chart on $M'$ and the collection of such charts forms a differentiable atlas on it.

II) We say that $M'$ is a $n'$-submanifold of $M$ if for all $p'\in M'$ there exist an open neighborhood $U_{p'}$ of $p'$ in $M$ and a differentiable mapping $\tilde{F}_{p'} \colon U_{p'}\to \mathbb{R}^{n'}$ s.t.:

i) The mapping $F_{p'}=\tilde{F}_{p'}|_{U_{p'} \cap M'}$ is one-one onto an open set $V$ of $\mathbb{R}^{n'}$;

ii) The inverse mapping $F_{p'}^{-1}\colon V \to M$ is differentiable.

If this is the case $(U_{p'}\cap M', F_{p'})$ is a local chart on $M'$ and the collection of such charts forms a differentiable atlas on it.

The difficult part is proving that II $\Rightarrow$ I, that is, given a collection of $(U_{p'}\cap M', F_{p'})$ use them to show that $M'$ is locally a slice of some coordinate system. How do you build a coordinate system like that?

The following is based on Warner's Foundations of differentiable manifolds and Lie groups, Proposition 1.35. Let $M, M', p', U_{p'}, \tilde{F}_{p'}$ as in II and put $\tilde{F}_{p'}=(y^1\ldots y^{n'})$. Since $F_{p'}$ has a differentiable inverse, the functions $y^1 \ldots y^{n'}$ must be independent at $p'$ and so they form part of a local chart $(W, y=(y^1\ldots y^n))$, where $W$ is an open neighborhood of $p'$ in the big manifold $M$. With no loss of generality let us assume that $y(p')=(0\ldots 0)$.

Now there is no need for the slice $\{p\in W \mid y^{n'+1}(p)=\ldots=y^{n}(p)=0\}$ to agree with $M'$.

So we need to tweak this coordinate system a little. Define a mapping $Pr\colon W \to W \cap M'$ by setting

$$Pr(p)=(y^1\ldots y^{n'})^{-1} (y^1(p) \ldots y^{n'}(p), 0 \ldots 0).$$

This mapping is best understood in coordinates: $Pr(p)$ is the unique point of $W\cap M'$ whose first $n'$ coordinates agree with the first $n'$ coordinates of $p$. It is clear that this mapping is differentiable (remember hypothesis (ii) above).

Define functions

$$z^i= \begin{cases} y^i & i=1\ldots n' \\ y^i-y^i \circ Pr & i=n'+1 \ldots n \end{cases};$$

those functions are independent at $p'$ and so they form a coordinate system in an open neighborhood $V$ of it. We have $\{p \in V \mid z^{n'+1}(p)=\ldots =z^n(p)=0\}=M' \cap V$: we have thus proven that $M'$ agrees locally with a slice of some coordinate system of $M$, that is, $M'$ verifies I. ////

-
Inverse function theorem maybe? If we write $F_{p'}=(y^1 \ldots y^{n'})$, then take local coordinates (for the big manifold $M$) $(x^1\ldots x^n)$, the mapping $(y^1\ldots y^{n'}, x^1 \ldots x^n)$ is differentiable and we can eliminate some $x^i$s (and rename the remaining) to get a mapping $(y^1\ldots y^{n'}, x^{n'+1} \ldots x^n)$ of full rank in $p'$. This is a coordinate system in a neighborhood of $p'$. Will it be the correct one? – Giuseppe Negro Mar 21 '11 at 20:00
It's quite late in my country, so the following answer is probably either wrong or bluntly oversophisticated: The map from $V$ to $M$ is differentiable and invertible, in particular the derivative does not vanish. It maps the coordinate directions within the local chart to tangential vectors of the submanifold. Choose a field of $n-n'$ vectors orthogonal to the tangential vector field. Now after possible restriction, vary the slice into the direction of these orthogonal normal vectors. Try to build a chart as in $I$ now. – shuhalo Mar 22 '11 at 1:30
Take $M'=\{x_1=x_2\}\subset \mathbb{R}^2$, $\tilde F(x_1+x_2):=(x_1+x_2)/2$. Then $dF$ is linear independent of both $dx_1$ and $dx_2$, but neither $x_1$ nor $x_2$ are constant on $M'$, contradicting your claim. Or did I get your proof wrong? – Florian Mar 22 '11 at 15:25
You mean $\tilde{F}(x_1, x_2)= (x_1+x_2)/2$, I think. Well, you're right. The construction I provided above, when applied to your example, gives the coordinate system $(y^1, x^1)=(\frac{x^1+x^2}{2}, x^1)$ and clearly $M'$ is not a slice of it. Now where's the error in my reasoning... Surely it must be somewhere around that "obvious identification". – Giuseppe Negro Mar 22 '11 at 18:07
I think I found a way out. Essentially definition II above prescribes the existence around $p'$ of a coordinate system $(y^1\ldots y^{n'}, x^{n'+1} \ldots x^n)$ in $M$ s.t. the first $n'$ coordinates, when restricted to $M'$, form a coordinate system on it. This is what you get when the natural inclusion $i\colon M' \to M$ is an immersion, and you can then prove our claim arguing like Warner in Proposition 1.35 of his Foundations of differentiable manifolds. Tomorrow I'll try to write more details. – Giuseppe Negro Mar 23 '11 at 0:56

This is not an answer but a quick observation. Consider $M:=\mathbb{R}^2$ and $M':=\{0\}\times [0,\infty) \cup [0,\infty)\times \{0\}$. Let $\tilde F: (x,y)\mapsto x-y$. Then $F:=\tilde F|_{M'}$ is a bijective mapping $M'\to \mathbb{R}$. This is not a counterexample because (ii) in (II) is not satisfied, but it shows that care has to be taken and (ii) is crucial.