The differential of Ad is ad

For $g,h\in G$, the identity $C_g\circ L_h=L_{C_g(h)}\circ C_g$ and the chain rule show that $(C_g{)}_{\ast }{Y}^L=({\mathrm{Ad}}_{g}Y{)}^L$: at the point $C_g(h)$ both sides equal $d(L_{C_g(h)}{)}_{e}d(C_g{)}_{e}Y$.

By [F5] and left invariance, ${\mathrm{\Phi }}_t(h)=h\exp (tX)=R_{\exp (tX)}(h)$ is the global flow of $X^L$: differentiating $L_h(\exp (tX))$ gives $X_{h\exp (tX)}^L$. Since left and right translations commute, $(R_a{)}_{\ast }{Y}^L$ is left invariant for every $a$. Therefore left translation fixes that field, and $C_{\exp (tX)}=L_{\exp (tX)}\circ R_{\exp (-tX)}$ gives $(C_{\exp (tX)}{)}_{\ast }{Y}^L=(R_{\exp (-tX)}{)}_{\ast }{Y}^L$.

Differentiate the last identity of step 1.2 at $t=0$. By the inverse-time convention and equality in [F6], its right side has derivative ${\mathcal{L}}_{X^L}{Y}^L=[X^L,Y^L]=[X,Y{]}_G^L$, where the last equality is [F4]. Step 1.1 identifies the left side with $({\mathrm{Ad}}_{\exp (tX)}Y{)}^L$. Evaluating the differentiated fields at $e$ thus yields ${\frac{d}{dt}\mid }_0{\mathrm{Ad}}_{\exp (tX)}Y=[X,Y{]}_G$.

The curve $t\mapsto \exp (tX)$ has initial velocity $X$ by [F5]. Apply the chain rule [F8] to $t\mapsto {\mathrm{Ad}}_{\exp (tX)}$ and then to the linear evaluation map $A\mapsto A(Y)$. Under $T_I\mathrm{GL}(\mathfrak{g})=\mathrm{End}(\mathfrak{g})$, step 2.1 becomes $(d(\mathrm{Ad}{)}_{e}X)(Y)=[X,Y{]}_G={\mathrm{ad}}_X(Y)$. Since this holds for every $Y$, $d(\mathrm{Ad}{)}_{e}X={\mathrm{ad}}_X$.

The final commutator identity follows from [F9], now with the map in [F9] identified by step 3.1 with the differential of the group adjoint representation.

A Lie group is nonempty and boundaryless. If $\dim G=0$, every tangent space in the claim is zero; in dimension one the Lie bracket and both sides are zero, while the same proof applies. Degenerate adjoint maps are allowed. The flows are global, so there is no endpoint issue, and no metric occurs. The only choice use is the stated ${\mathrm{A}\mathrm{C}}_{\omega }$, inherited through [F2]--[F7]; fixing two tangent vectors and differentiating their specified curves adds no choice. No biconditional is asserted.