The Lie-group exponential map is smooth with identity differential at zero

On the product manifold $M=G\times \mathfrak{g}$, define ${\mathcal{X}}_{(g,Y)}:=(d(L_g{)}_{e}Y,0)\in T_{g}G\times T_Y\mathfrak{g}=T_{(g,Y)}M\mathrm{.}$ Its first component is the smooth map supplied by [F3], and its second component is the zero field on the vector space $\mathfrak{g}$. Hence $\mathcal{X}$ is a smooth vector field on $M$.

For $(g,Y)\in M$, define $c_{g,Y}:\mathbb{R}\to M$ by $c_{g,Y}(t)=(g{\gamma }_Y(t),Y)$. By [F4], [F8], and $L_g\circ L_{{\gamma }_Y(t)}=L_{g{\gamma }_Y(t)}$, $c_{g,Y}^{\mathrm{\prime }}(t)=(d(L_g{)}_{{\gamma }_Y(t)}d(L_{{\gamma }_Y(t)}{)}_{e}Y,0)=(d(L_{g{\gamma }_Y(t)}{)}_{e}Y,0)={\mathcal{X}}_{c_{g,Y}(t)}\mathrm{.}$ Thus $c_{g,Y}$ is an integral curve of $\mathcal{X}$ through $(g,Y)$ and is defined on all of $\mathbb{R}$. Every maximal integral curve of $\mathcal{X}$ is therefore global. By [F5], the global flow is smooth and is $\mathrm{\Psi }(t,(g,Y))=(g{\gamma }_Y(t),Y)\mathrm{.}$

Restricting this smooth flow to $(t,(e,Y))$ and projecting to $G$ shows that $(t,Y)\mapsto {\gamma }_Y(t)$ is smooth. Restricting further to $t=1$ gives the map $Y\mapsto {\gamma }_Y(1)={\exp }_G(Y)$, which is smooth by [F2].

By [F6] with $a=0$ and [F7], ${\exp }_G(0)={\gamma }_X(0)=e$. Fix $X\in \mathfrak{g}$ and consider $q_X(a)=aX$. Applying [F8] to ${\exp }_G\circ q_X$ and then [F6] gives $d({\exp }_G{)}_0(X)={\frac{d}{da}\mid }_{a=0}{\exp }_G(aX)={\frac{d}{da}\mid }_{a=0}{\gamma }_X(a)={\gamma }_X^{\mathrm{\prime }}(0)=X\mathrm{.}$ Hence $d({\exp }_G{)}_0$ is the identity under $T_0\mathfrak{g}\simeq \mathfrak{g}$.

Lie groups are nonempty and boundaryless. If $\dim G=0$, then $\mathfrak{g}=0$, the exponential maps the unique vector to $e$, and its differential is the identity of the zero space; in dimension one the proof is unchanged. The global curves in step 2.1 remove finite-time endpoint issues. No metric or nondegeneracy condition occurs. The only choice use is the stated ${\mathrm{A}\mathrm{C}}_{\omega }$, inherited through [F2]--[F4] and especially the smooth tangent-bundle trivialization [F3]; forming one product field and restricting its flow adds no choice. No biconditional is asserted.