[proofplan]
We realise $\mathfrak g$ as the [Lie algebra](/page/Lie%20Algebra) of a finite-dimensional real Lie group $G$ using Lie's third theorem, noting that this integration result is a prerequisite not yet in the wiki: Lie's third theorem. We then choose exponential coordinates near the identity of $G$ and pull the group multiplication back to a partial operation near $0\in\mathfrak g$. The Baker--Campbell--Hausdorff convergence theorem identifies this pulled-back multiplication with the BCH series after shrinking the neighbourhood. The local identity, inverse, associativity, and smoothness are inherited from the corresponding properties of the Lie group operations on $G$.
[/proofplan]
[step:Choose an integrating Lie group and exponential coordinates near the identity]
By Lie's third theorem, there exists a finite-dimensional real Lie group $G$ whose Lie algebra is identified with $\mathfrak g$. Let $e\in G$ denote the identity element. Let
\begin{align*}
\exp_G:\mathfrak g\to G
\end{align*}
denote the Lie group exponential map.
By the local diffeomorphism theorem for the Lie group exponential map, there are open neighbourhoods $V\subset \mathfrak g$ of $0$ and $W\subset G$ of $e$ such that
\begin{align*}
\exp_G|_V:V\to W
\end{align*}
is a diffeomorphism. Define
\begin{align*}
\log_G:W\to V
\end{align*}
to be its inverse.
[guided]
The goal is to convert the abstract Lie algebra operation into an actual local multiplication. To do that, we first choose a genuine Lie group whose infinitesimal Lie algebra is the given $\mathfrak g$. Lie's third theorem gives a finite-dimensional real Lie group $G$ with Lie algebra identified with $\mathfrak g$.
Let $e\in G$ be the identity element, and let
\begin{align*}
\exp_G:\mathfrak g\to G
\end{align*}
be the Lie group exponential map. The exponential map need not be globally injective or globally surjective, so we use only its local behaviour at $0\in\mathfrak g$. The local diffeomorphism theorem for the exponential map says that there are open neighbourhoods $V\subset\mathfrak g$ of $0$ and $W\subset G$ of $e$ for which
\begin{align*}
\exp_G|_V:V\to W
\end{align*}
is a diffeomorphism. We define
\begin{align*}
\log_G:W\to V
\end{align*}
to be the inverse diffeomorphism. These exponential coordinates are the bridge between the group multiplication in $G$ and the desired local operation on $\mathfrak g$.
[/guided]
[/step]
[step:Pull back the group multiplication to a partial product on $\mathfrak g$]
Let
\begin{align*}
m_G:G\times G\to G
\end{align*}
be the smooth multiplication map of $G$, given by $m_G(g,h)=gh$. Define the [open set](/page/Open%20Set)
\begin{align*}
\Omega_V:=\{(X,Y)\in V\times V:\exp_G(X)\exp_G(Y)\in W\}.
\end{align*}
This set is open because the map $(X,Y)\mapsto \exp_G(X)\exp_G(Y)$ is smooth, hence continuous, and $W$ is open. It contains $(0,0)$ because $\exp_G(0)=e$ and $ee=e\in W$.
Define
\begin{align*}
\mu:\Omega_V\to V
\end{align*}
by
\begin{align*}
\mu(X,Y)=\log_G(\exp_G(X)\exp_G(Y)).
\end{align*}
The map $\mu$ is smooth because it is the composition of the smooth map $(X,Y)\mapsto \exp_G(X)\exp_G(Y)$ with the smooth map $\log_G:W\to V$.
[/step]
[step:Shrink the domain so the BCH series equals the pulled-back product]
Choose a norm $\|\cdot\|_{\mathfrak g}$ on the finite-dimensional real [vector space](/page/Vector%20Space) $\mathfrak g$. Let $[\cdot,\cdot]:\mathfrak g\times\mathfrak g\to\mathfrak g$ denote the Lie bracket. Since $\mathfrak g$ is finite-dimensional, after multiplying the norm by a positive constant if necessary, we may assume
\begin{align*}
\|[A,B]\|_{\mathfrak g}\leq \|A\|_{\mathfrak g}\|B\|_{\mathfrak g}
\end{align*}
for all $A,B\in\mathfrak g$.
By [citetheorem:8797], the Dynkin Baker--Campbell--Hausdorff Lie series converges whenever
\begin{align*}
\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2.
\end{align*}
The same BCH theorem, applied to the integrating Lie group $G$ with Lie algebra $\mathfrak g$, gives an open neighbourhood $N\subset\mathfrak g\times\mathfrak g$ of $(0,0)$ such that, for every $(X,Y)\in N$, the BCH series converges, $\operatorname{BCH}(X,Y)\in V$, $\exp_G(X)\exp_G(Y)\in W$, and
\begin{align*}
\exp_G(\operatorname{BCH}(X,Y))=\exp_G(X)\exp_G(Y).
\end{align*}
Choose an open neighbourhood $U\subset V$ of $0$. Since $\mu(0,0)=0$ and $\mu$ is continuous, shrink to an open neighbourhood $\Omega\subset \Omega_V\cap N\cap(U\times U)\cap\mu^{-1}(U)$ of $(0,0)$. For $(X,Y)\in\Omega$, applying $\log_G$ to the preceding identity gives
\begin{align*}
\mu(X,Y)=\operatorname{BCH}(X,Y).
\end{align*}
Thus the map
\begin{align*}
*: \Omega\to U
\end{align*}
defined by $X*Y=\mu(X,Y)$ satisfies
\begin{align*}
X*Y=\operatorname{BCH}(X,Y)
\end{align*}
for every $(X,Y)\in\Omega$.
[guided]
We now identify the pulled-back multiplication with the BCH expression. First choose a norm $\|\cdot\|_{\mathfrak g}$ on the finite-dimensional real vector space $\mathfrak g$. The bilinear bracket map
\begin{align*}
[\cdot,\cdot]:\mathfrak g\times\mathfrak g\to\mathfrak g
\end{align*}
is continuous, so there is a constant $C_0>0$ such that
\begin{align*}
\|[A,B]\|_{\mathfrak g}\leq C_0\|A\|_{\mathfrak g}\|B\|_{\mathfrak g}
\end{align*}
for all $A,B\in\mathfrak g$. Replacing the norm by $C_0\|\cdot\|_{\mathfrak g}$ if $C_0>0$, and leaving it unchanged if $C_0\leq 1$, gives a norm for which
\begin{align*}
\|[A,B]\|_{\mathfrak g}\leq \|A\|_{\mathfrak g}\|B\|_{\mathfrak g}.
\end{align*}
Now [citetheorem:8797] applies to this finite-dimensional real Lie algebra with this norm. It says that the Dynkin BCH Lie series converges whenever
\begin{align*}
\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2.
\end{align*}
The same theorem also supplies the local exponential-product identity for the integrating Lie group $G$: there is an open neighbourhood $N\subset\mathfrak g\times\mathfrak g$ of $(0,0)$ such that, for every $(X,Y)\in N$, the BCH series converges, $\operatorname{BCH}(X,Y)\in V$, $\exp_G(X)\exp_G(Y)\in W$, and
\begin{align*}
\exp_G(\operatorname{BCH}(X,Y))=\exp_G(X)\exp_G(Y).
\end{align*}
We now redeclare the pulled-back product so the local comparison is self-contained. Define
\begin{align*}
\Omega_V:=\{(X,Y)\in V\times V:\exp_G(X)\exp_G(Y)\in W\}
\end{align*}
and define
\begin{align*}
\mu:\Omega_V\to V
\end{align*}
by
\begin{align*}
\mu(X,Y)=\log_G(\exp_G(X)\exp_G(Y)).
\end{align*}
Choose an open neighbourhood $U\subset V$ of $0$. Since $\mu(0,0)=0$ and $\mu$ is continuous, we may shrink the product domain to an open neighbourhood $\Omega\subset\Omega_V\cap N\cap(U\times U)\cap\mu^{-1}(U)$ of $(0,0)$. For such $(X,Y)$, the product $\exp_G(X)\exp_G(Y)$ lies in $W$ by the definition of $\Omega_V$, so applying $\log_G:W\to V$ to the displayed identity gives
\begin{align*}
\log_G(\exp_G(X)\exp_G(Y))=\operatorname{BCH}(X,Y).
\end{align*}
The left-hand side is exactly $\mu(X,Y)$. Therefore the operation
\begin{align*}
*: \Omega\to U
\end{align*}
defined by $X*Y=\mu(X,Y)$ is precisely the BCH operation on its domain.
[/guided]
[/step]
[step:Pull back the identity and inverse laws from the Lie group]
For every $X\in U$ with $(0,X)\in\Omega$ and $(X,0)\in\Omega$, we have
\begin{align*}
0*X=\log_G(\exp_G(0)\exp_G(X))=\log_G(e\exp_G(X))=X
\end{align*}
and
\begin{align*}
X*0=\log_G(\exp_G(X)\exp_G(0))=\log_G(\exp_G(X)e)=X.
\end{align*}
Thus $0$ is a two-sided identity wherever the products are defined.
For every $X\in U$ such that $-X\in U$ and the products $(X,-X)$ and $(-X,X)$ lie in $\Omega$, the exponential identity for one-parameter subgroups gives
\begin{align*}
\exp_G(-X)=\exp_G(X)^{-1}.
\end{align*}
Therefore
\begin{align*}
X*(-X)=\log_G(\exp_G(X)\exp_G(-X))=\log_G(e)=0
\end{align*}
and
\begin{align*}
(-X)*X=\log_G(\exp_G(-X)\exp_G(X))=\log_G(e)=0.
\end{align*}
Hence the local inverse of $X$ is $-X$ wherever the relevant products are defined.
[/step]
[step:Pull back associativity on the common local domain]
Let $X,Y,Z\in U$ be such that all products appearing below are defined and lie in the chosen local chart. Then
\begin{align*}
\exp_G((X*Y)*Z)=\exp_G(X*Y)\exp_G(Z).
\end{align*}
By the definition of the pulled-back product,
\begin{align*}
\exp_G(X*Y)=\exp_G(X)\exp_G(Y).
\end{align*}
Thus
\begin{align*}
\exp_G((X*Y)*Z)=(\exp_G(X)\exp_G(Y))\exp_G(Z).
\end{align*}
Associativity in the Lie group $G$ gives
\begin{align*}
(\exp_G(X)\exp_G(Y))\exp_G(Z)=\exp_G(X)(\exp_G(Y)\exp_G(Z)).
\end{align*}
Using the definition of the pulled-back product again,
\begin{align*}
\exp_G(X)(\exp_G(Y)\exp_G(Z))=\exp_G(X)\exp_G(Y*Z)=\exp_G(X*(Y*Z)).
\end{align*}
Both $(X*Y)*Z$ and $X*(Y*Z)$ lie in $V$, and $\exp_G|_V$ is injective. Therefore
\begin{align*}
(X*Y)*Z=X*(Y*Z).
\end{align*}
This proves associativity on the common domain where both sides are defined.
[/step]
[step:Conclude that the BCH product is a local Lie group law]
The map $*: \Omega\to U$ is smooth because it equals the smooth pulled-back product $\mu$ on $\Omega$. The preceding steps prove that $0$ is a two-sided identity, that $X^{-1}=-X$ wherever the inverse products are defined, and that associativity holds whenever both associated products are defined. Since $X*Y=\operatorname{BCH}(X,Y)$ on $\Omega$, the BCH operation defines the claimed local Lie group law on a sufficiently small neighbourhood of $0\in\mathfrak g$.
[/step]
