I am reading Introduction to Smooth Manifolds by John M. Lee, and I have a question about the proof of a theorem about canonical form for commuting vector fields. The statement and the proof of the theorem (Theorem 9.46 in the book) goes as follows:
Theorem. Let $M$ be a smooth $n$-manifold, and let $(V_1,\dots,V_k)$ be a linearly independent $k$-tuple of smooth commuting vector fields on an open subset $W\subseteq M$. For each $p\in W$, there exists a smooth coordinate chart $(U,(s_i))$ centered at $p$ such that $V_i=\partial/\partial s^i$ for $i=1,\dots ,k$/ If $S\subseteq W$ is an embedded codimension-$k$ submanifold and $p$ is a point of $S$ such that $T_p S$ is complementary to the span of $(V_1\mid _p,\dots V_k\mid _p)$, then the coordinates can also be chosen such that $S\cap U$ is the slice defined by $s^1=\cdots=s^k=0$.
Proof. Choose a slice chart $(U,(x^i))$ for $S$ centered at $p$, so that $U\cap S$ is equal to the slice $\{x\in U\mid x^1=\cdots =x_k=0\}$. Because the theorem is local, it suffices to consider the case where $U$ is an open set of $\mathbb{R}^n$.
Let $\theta_i$ denote the flow of $V_i$ for $i=1,\dots, k$, and choose $\varepsilon>0$ and a neighbrohood $Y$ of $p$ such that the composition $(\theta_1)_{t_1} \circ \cdots \circ(\theta_k)_{t_k}$ is defined on $Y$ and maps $Y$ into $U$ whenever $|t_1|,\dots |t_k|$ are all less than $\varepsilon$. Define $\Omega\subseteq \mathbb{R}^{n-k}$ by $$\Omega=\{(s^{k+1},\dots,s^n)|(0,\dots,0,s^{k+1},\dots,s^n)\in Y\},$$ and define $\Phi:(-\varepsilon,\varepsilon)^k\times \Omega\to U$ by $$\Phi(s^1,\dots s^n)=(\theta_1)_{s^1} \circ \cdots \circ(\theta_k)_{s^k}(0,\dots,0,s^{k+1},\dots ,s^n).$$ The hypothesis that $\theta_i$ commutes ensures us that $\partial/\partial s^i$ is $\Phi$-related to $V_i$ for $i=1,\dots ,k$. By construction, we also have $d\Phi_0(\partial/\partial s^i|_0)=\partial/\partial x^i \mid _p$ for $i=k+1,\dots, n$; it follows that the differential $d\Phi _0$ of $\Phi$ at the origin is invertible, so $\Phi$ restricts a diffeomorphism from a neighborhood of $0$ onto an open set $\tilde U$ of $M$. The chart $(\tilde U,\varphi):=(\tilde U, \Phi^{-1})$ is the desired slice chart for $S$. $\square$
I do not understand why the chart $(\tilde U,\varphi)$ a slice chart for $S$. For sure, by construction we have $\Phi (\{0\}\times \Omega)=S\cap Y$, so if $q\in \tilde U$ satisfies $\varphi(q)\in \{0\}\times \mathbb{R}^{n-k}$, then $q$ has to lie in $S$. However, (if my understanding is correct) the construction above does not exclude the possibility that $\varphi(\tilde U\cap S)\supsetneq \varphi(\tilde U)\cap (\{0\}\times \mathbb{R}^{n-k})$.
So the question really boils down to finding some neighborhood of $0$ whose point is mapped into $S$ by $\Phi$ if and only if its first $k$ coordinates are all $0$; and intuitively, it is not hard to convince ourselves that such a neighborhood does exist. But I have been having a hard time proving it. Can anyone help me? Thanks in advance.