Derivative of the inclusion of a submanifold

I know there are other questions similar to this one, but I just want you to tell me if what I'm doing is rigth and how to improve it. The problem is the following: (I'm using the definitions by Guillemin & Pollack)

Let $Y\subset R^N$ be an $l-$dimensional manifold and suppose $X$ is a $k-$dimensional submanifold of $Y$. Let $\imath:X\rightarrow Y$ be the inclusion map. Then for every $x\in X$, the differential $d\imath_x:T_xX\rightarrow T_xY$ is also the inclusion map.

This is my solution: Let's take $x\in X$. Consider a parametrization $\phi:U\subset R^l\rightarrow V$ of $Y$ around $x$ such that $0\in U$ and $\phi(0)=x$. Since the definitions don't depend on the parametrizations we can consider the following parametrization of $X$ around $x$: We know that there exists an open set $\mathcal V$ in $R^N$ such that $V=\mathcal V\cap Y$, so we can consider the open set $\tilde V=\mathcal V\cap X$ in $X$. Define $\tilde\phi:\tilde U\subset R^k\rightarrow\tilde V$ as $$\tilde\phi(a_1,\dots,a_k)=\phi(a_1,\dots,a_k,0,\dots,0),$$ where $\tilde U$ is the inverse image of $U$ under the canonical inclusion $\jmath:R^k\hookrightarrow R^l$. Clearly, $\tilde\phi$ is smooth, because $\tilde\phi=\phi\circ\jmath$. Moreover, $\tilde\phi$ is a diffeomorphism with inverse $\tilde\phi^{-1}=\pi\circ\phi\vert_{\tilde V}^{-1}$, where $\pi:R^k\times R^{l-k}\rightarrow R^k$ is the projection on $R^k$. Now, let $v\in T_xX$, then $v=d\tilde\phi_0(a)$ with $a\in R^k$. Observe that $v=d\phi_0(\jmath(a))$. Then $$d\imath_x(v)=d\phi_0\circ d\tilde\imath_0\circ(d\tilde\phi_0)^{-1}(v),$$ where $\tilde\imath=\phi^{-1}\circ\imath\circ\tilde\phi=\jmath\vert_{\tilde U}$. Since $d\tilde\imath_0=\jmath$, then we have $$d\imath_x(v)=d\phi_0\circ d\tilde\imath_0\circ(d\tilde\phi_0)^{-1}(v)=d\phi_0(\jmath(a))=v.$$ So, $d\imath_x$ is the inclusion map.

This is certainly a valid proof, and whilst the method behind it is very intuitive, actually writing out what's being doing is very messy, especially considering the problem feels like it should be "obvious".

A much "nicer" proof comes from using the following equivalent definition of derivative, if $f:X\rightarrow Y$ is a smooth map of manifolds embedded in $\mathbb{R}^N,\mathbb{R}^M$ respectively, then we define the derivative of $f$ at $x$, $df_x:T_xX\rightarrow T_{f(x)}Y$ by taking a smooth extension of $f$, $F:U\rightarrow\mathbb{R}^M$ (where $U$ is an open subset of $\mathbb{R}^N$) and taking $df_x$ to be the restriction of $dF_x$ to $T_xX$.

You can show that this is (well) defined (i.e. a map to $T_{f(x)}Y$, independent of choice of extension) by showing that for any given extension and choice of parameterisations $\phi$ on $X$ and $\psi$ on $Y$, $dF=(d\psi)(d\bar f)(d\phi)^{-1}$ (on suitable domains). Note that the left hand side is independent of chart, and the right hand side is independent of extension, so both expressions are independent of both! I count at least three birds with one short proof (which is one reason that I much prefer this definition of derivative) because simply showing this definition is well defined also shows that your definition is well defined, and that the two are the same, providing you multiple methods for computation.

Anyway, using this definition, with the notation as in your question, the inclusion map $\iota :X \rightarrow Y$ is just the restriction of the identity map $I_N$ on $\mathbb{R}^N$. Thus $d\iota_x$ is the restriction of the derivative of $I_N$ to $T_xX$, i.e. the inclusion map. Done in barely three lines, with no computation!

Here's a "counterexample" to the original post as requested. We'll define spaces $X \subset Y$ and a parametrization $\phi $ so that the suggested function $\tilde \phi $ is not well defined. The counterexample has a lot of pieces so I suggest making some sketches.

Let the ambient space be ${\rm I\!R}^3$. Let $Y = S^2 $ be the sphere in ${\rm I\!R}^3$ and let $$X = \left\{ {\left( {x,y,{1 \over {\sqrt 2 }}} \right)\,\,\left| {\,x^2 + y^2 = {1 \over 2}} \right.} \right\}$$

be the $45^0 $ N latitude line on the $S^2 $ globe. Let $x = \left( {{1 \over 2},{1 \over 2},{1 \over {\sqrt 2 }}} \right) \in X$ . Let $\phi :U \to V$ where $U = \{(x,y)\,|\, x^2+y^2<1/4\}$ is the open disc of radius 1/4 centered at $0$ in the x-y plane, and $$\phi \left( {x,y} \right) = \left( {x + {1 \over 2},y + {1 \over 2},\sqrt {1 - \left( {x + {1 \over 2}} \right)^2 - \left( {y + {1 \over 2}} \right)^2 } } \right)$$

and $V = \phi \left( U \right)$ which is the projection onto the upper hemisphere of the open disc of radius 1/4 centered at the point $\left( {{1 \over 2},{1 \over 2}} \right)$ in the x-y plane. Then $\phi $ parameterizes $Y$ around $x$ with $0 \in U$ and $\phi \left( 0 \right) = x$ . Furthermore, $ \tilde V = V \cap X $ is the open segment of $X$ that passes through $V$ . And since the canonical immersion (not "canonical inclusion") in our case is $j: {\rm I\!R}^1 \to {\rm I\!R}^2$, we have $\tilde U = j^{ - 1} \left( U \right) = \left( { - {1 \over 4},{1 \over 4}} \right)$ .

The suggested function definition is $\tilde \phi :\tilde U \to \tilde V$ , $\tilde \phi \left( x \right) = \phi \left( {x,0} \right)$ . We claim this function is not well-defined because $\tilde \phi $ does not take $\tilde U$ to $\tilde V$ . The image $ \tilde \phi \left( {\tilde U} \right) $ is the projection onto the upper hemisphere of the open line segment between the points $\left( {{1 \over 4},{1 \over 2}} \right)$ and $\left( {{3 \over 4},{1 \over 2}} \right)$ in the x-y plane. This makes $ \tilde \phi \left( {\tilde U} \right) $ a segment of the circle obtained by slicing the sphere with the plane $y = {1 \over 2}$ . Meanwhile $\tilde V$ is a segment of the circle obtained by slicing the sphere with the plane $z = {1 \over {\sqrt 2 }}$ . Therefore $ \tilde \phi \left( {\tilde U} \right) \not\subset \tilde V $. In fact, when you sketch it out, you'll see that $ \tilde \phi \left( {\tilde U} \right) $ and $\tilde V$ intersect only at $x$ .

The proof in the original post may have been philosophically misguided as it seems that it was trying to use the Local Immersion Theorem from Section 1.3 to prove the inclusion theorem presented in Section 1.2.

I'm pretty sure there's a problem with your proof. The function $\tilde \phi$ defined as $\tilde \phi \left( {a_1 , \ldots ,a_k } \right) = \phi \left( {a_1 , \ldots ,a_k ,0, \ldots ,0} \right)$ doesn't necessarily take $\tilde U$ into $\tilde V$. I was able to construct a "counterexample" where $\tilde \phi \left( {\tilde U} \right) \not\subset \tilde V$. Unfortunately, I can't see how to modify your proof to fix it.