Differential of a Lie-group homomorphism is a Lie-algebra homomorphism

Fix $X\in \mathfrak{g}$. By [F5], $X$ and $d{F}_{e}X$ have left-invariant extensions $X^L$ on $G$ and $(d{F}_{e}X{)}^L$ on $H$. For every $g\in G$, the homomorphism law [F3] gives $F\circ L_g=L_{F(g)}\circ F$. Therefore [F8] gives $d{F}_g(X_g^L)=d{F}_{g}d(L_g{)}_{e}X=d(L_{F(g)}{)}_{e_H}d{F}_{e}X=(d{F}_{e}X{)}_{F(g)}^L\mathrm{.}$ Thus $X^L$ and $(d{F}_{e}X{)}^L$ are $F$-related.

Apply [F4] to the related pairs from step 1.1 for $X$ and $Y$. Then $[X^L,Y^L]$ is $F$-related to $[(d{F}_{e}X{)}^L,(d{F}_{e}Y{)}^L]$. Evaluating relatedness at $e$ and using [F6] on both groups yields $d{F}_e([X,Y{]}_{\mathfrak{g}})=[d{F}_{e}X,d{F}_{e}Y{]}_{\mathfrak{h}}\mathrm{.}$

By [F7], $d{F}_e$ is linear, and step 2.1 proves bracket preservation. Hence $d{F}_e$ is a Lie-algebra homomorphism by [F2].

Lie groups are nonempty and boundaryless. If either Lie algebra is zero-dimensional, the same related-field calculation applies and all relevant source vectors or target values are zero; in dimension one the proof is unchanged. No metric, nondegeneracy, interval, or endpoint occurs. The only choice use is the stated ${\mathrm{A}\mathrm{C}}_{\omega }$, inherited through [F5] and [F6]; fixing two tangent vectors adds no choice. No biconditional is asserted.