Question about the normal bundle of a totally geodesic submanifold of a Cartan-Hadamard manifold I'm reading the exposition in Lang's Fundamentals of Differential Geometry of the following generalization of the Cartan-Hadamard theorem:
Suppose $X$ is a Cartan-Hadamard manifold (i.e. a complete, simply connected manifold with everywhere nonpositive sectional curvature) and $Y$ is a complete totally geodesic submanifold of $X$. Let $NY$ be the normal bundle of $Y$ in $X$, and let $\exp_{NY}: NY\rightarrow X$ be the restriction of the exponential map to $NY$. Then $\exp_{NY}$ is a diffeomorphism. This is Theorem 2.5 of Chapter X.
I'm confused about a detail in the proof of the preceding Theorem, 2.4. Fix $y_0\in Y$, and for each $y\in Y$, let $P_{y_0}^y$ denote parallel transport from $T_{y_0}X$ to $T_{y}X$ along the unique geodesic connecting $y_0$ to $y$. Now, define the smooth map $E:Y\times N_{y_0}Y\rightarrow X$ by $E(y,v)=\exp_y(P^y_{y_0}v)$.
At the bottom of page 273, Lang claims that $dE_{(y,v)}(z,0)$ is orthogonal to $dE_{(y,v)}(0,w)$ for any $y\in Y,v\in N_{y_0}Y,  z\in T_yY,w\in N_{y_0}Y$.
I don't understand why this is true. He says it follows from the Gauss Lemma (Lemma VIII.5.6), but I can't figure out how it follows. I'm probably missing something simple. Does anyone know why those things are orthogonal?  
Also, Lang is the only reference I can find for the fact that $\exp_{NY}:NY\rightarrow X$ is a diffeomorphism. Does anyone know if this exists elsewhere in the literature?
Thanks.
 A: I'm still not sure about that detail in the proof in Lang,
but here's a slightly different proof that $\exp_{NY}:NY\rightarrow X$ is a diffeomorphism.
Step one: $\exp_{NY}$ is surjective.
To see this, let $x\in X\setminus Y$. Let $B$ be a closed metric ball centered at $x$ containing some point of $Y$.
Since $X$ is complete, $B$ is compact, and since $Y$ is closed in $X$, $B\cap Y$ is compact.
Thus, there is $y_0\in B\cap Y$ which is closest to $x$, and so we have $d(x,y_0) = d(x, B\cap Y) = d(x, Y)$.
By differentiating $y\mapsto d(x,y)$ along any curve in $Y$ through $y_0$, we find that the geodesic connecting $y_0$
to $x$ is normal to $Y$ at $y_0$. In other words, if $\gamma:[0,1]\rightarrow X$ is the geodesic with $\gamma(0)=y_0$, $\gamma(1)=x$,
then $\gamma'(0)\in NY_{y_0}$. So $\exp_{NY}(\gamma'(0))=x$, and we have surjectivity.
Step two: $\exp_{NY}$ is injective.
Suppose there were distinct $v_0, v_1 \in NY$ such that $\exp_{NY}(v_0) = \exp_{NY}(v_1)=x$.
If $v_0,v_1$ were based at the same point of $Y$, then the exponential map based at that point would fail to be injective,
contradicting the Cartan-Hadamard theorem. So $v_1, v_2$ are based at distinct points $y_1,y_2\in Y$.
Let $\gamma:[0,1]\rightarrow Y$ be the geodesic with $\gamma(0)=y_0, \gamma(1)=y_1$. 
Then we have $\frac{d}{dt}|_{t=0}d(x,\gamma(t)) = \frac{d}{dt}|_{t=1}d(x, \gamma(t))=0$,
because the geodesic connecting $y_0$ to $x$ is normal to $\gamma'(0)$ at $y_0$ and
the geodesic connecting $y_1$ to $x$ is normal to $\gamma'(1)$ at $y_1$. This contradicts 
the convexity of the distance function of $X$.
So $\exp_NY$ is bijective.
As Deane pointed out in the comments, it now suffices to show
Step three: The differential of $\exp_{NY}$ is everywhere injective.
For this, fix $y_0\in Y$, and for each $y\in Y$, let $P_{y_0}^{y}$ denote parallel transport
from $y_0$ to $y$. Then the map $Y\times NY_{y_0} \rightarrow NY$ given by $(y, v)\mapsto P_{y_0}^y v$
is a diffeomorphism, so it suffices to show that the map $E$ defined as the composition $Y\times NY_{y_0} \rightarrow NY \stackrel{\exp_{NY}}{\rightarrow}X$
has everywhere injective differential.
To this end, choose $(y,v)\in Y\times NY_{y_0}$ and nonzero $(z,w)\in T_yY\times NY_{y_0}$.
We need to show $dE_{(y,v)}(z,w)\neq 0$. Let $\gamma(t)$ be the geodesic passing through $y$ at time 0 with velocity $z$.
We need to show that $\frac{d}{dt}|_{t=0} \exp_{\gamma(t)} P_{y_0}^{\exp(\gamma(t))} (v+tw)$ is not zero. Let 
$\alpha(s)= \exp_y P^{y}_{y_0}(sv)$.
Let $\Gamma(s,t) = \exp_{\gamma(t)} P_{y_0}^{\exp(\gamma(t))} s(v+tw)$, and 
$J(s) = \frac{\partial}{\partial t} \Gamma(s,0)$. $J$ is a Jacobi field along the geodesic $\alpha$. Set $f(s) = \langle J(s), J(s) \rangle$. We will show $f(s)>0$ for $s>0$. 
Setting $s=1$ will then yield the desired result.
Compute 
\begin{align*}
f'(0) &= 2\langle \frac{D}{\partial s}\frac{\partial}{\partial t}\Gamma(0,0), \frac{\partial}{\partial t}\Gamma(0,0) \rangle\\
       &= 2\langle \frac{D}{\partial t}\frac{\partial}{\partial s}\Gamma(0,0), \frac{\partial}{\partial t}\Gamma(0,0) \rangle\\
       &= 2\langle \frac{D}{\partial t}|_{t=0}P_{y_0}^{\exp(\gamma(t))} (v+tw), \frac{d}{dt}|_{t=0}\gamma(t) \rangle\\
       &=2 \frac{\partial}{\partial t}|_{t=0} \langle P_{y_0}^{\exp(\gamma(t))} (v+tw), \frac{d}{dt}\gamma(t) \rangle\\
       &=0,
\end{align*}
since $P_{y_0}^{\exp(\gamma(t))} (v+tw) \in NY$ and $\frac{d}{dt}\gamma(t)\in TY$ for all $t$.
Also,
\begin{align*}
f''(s) &= 2\langle J'(s), J'(s)  \rangle + 2\langle J''(s), J(s) \rangle\\ &= 2\langle J'(s), J'(s)  \rangle - 2\langle R(\alpha'(s), J(s))\alpha'(s), J(s) \rangle\\&\geq 0.
\end{align*}
Now, $J(0) = z$, so if $z\neq 0$, then $f(0)>0$, which combined with the two computations above, proves $f(s)>0$ for all $s>0$.
If $z=0$, then $w\neq 0$ and $J'(0)=w$, so $f''(0)>0$, and again we conclude $f(s)>0$ for all $s>0$.
