[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.[/step]

[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: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$.[/step]

[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: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]