Left-invariant vector fields are complete

Let $c:I\to G$ be the maximal integral curve of $X$ with $c(0)=e$, supplied by [F3]. Since $I$ is open and contains $0$, fix $\delta >0$ with $(-\delta ,\delta )\subseteq I$.

For $s\in I$, define ${\eta }_s(t)=c(s)c(t-s)$ on $(s-\delta ,s+\delta )$. By [F4], [F5], and left invariance [F2], ${\eta }_s^{\mathrm{\prime }}(t)=d(L_{c(s)}{)}_{c(t-s)}{c}^{\mathrm{\prime }}(t-s)=d(L_{c(s)}{)}_{c(t-s)}{X}_{c(t-s)}=X_{{\eta }_s(t)}\mathrm{.}$ Also ${\eta }_s(s)=c(s)c(0)=c(s)$. After shifting the parameter by $s$, uniqueness in [F3] shows that ${\eta }_s$ and $c$ agree wherever their domains overlap near $s$, and hence on their whole interval overlap by the same local uniqueness argument.

Suppose the right endpoint $b=\sup I$ were finite. Choose $s\in I$ with $b-\delta \mathrm{/}2<s<b$. Then $s+\delta >b$, while step 2.1 makes $c$ and ${\eta }_s$ agree on the nonempty overlap. Splicing them therefore gives an integral curve through $e$ on the strictly larger interval $I\cup (s-\delta ,s+\delta )$, contradicting maximality in [F3]. The identical argument at the left endpoint, using $s$ with $a<s<a+\delta \mathrm{/}2$ if $a=\inf I$ were finite, excludes a finite left endpoint. Thus $I=\mathbb{R}$.

For an arbitrary $p\in G$, define $c_p(t)=pc(t)$ on all of $\mathbb{R}$. The calculation of step 2.1 with $c(s)$ replaced by the fixed element $p$ proves that $c_p$ is an integral curve of $X$, and $c_p(0)=p$. Its domain is already all of $\mathbb{R}$, so maximal uniqueness [F3] and [F6] show that $X$ is complete.

By [F7], completeness is equivalent to the maximal flow domain being all of $\mathbb{R}\times G$, which proves the final formulation in the statement.

A Lie group is nonempty. In dimension zero every smooth vector field is zero and its integral curves are constant; in dimension one the extension proof above is unchanged. Lie groups are boundaryless, so no boundary or finite-time endpoint exception remains, and no metric or nondegeneracy enters. The stated ${\mathrm{A}\mathrm{C}}_{\omega }$ is inherited through [F2] and the smooth tangent-field framework; choosing one $\delta$ and one $s$ inside a single nonempty interval uses no family choice, and the endpoint argument adds no choice. The theorem is a direct assertion plus the supplied equivalence in [F7]; both directions of that cited equivalence are available.