[proofplan]
We use Dynkin's explicit form of the Baker--Campbell--Hausdorff series and estimate each nested commutator by the product of the norms of its entries. The bracket submultiplicativity hypothesis reduces absolute convergence of the Lie series to convergence of a scalar majorant. The scalar majorant gives precisely the radius $\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2$. In the matrix group case, a fixed [Lie algebra](/page/Lie%20Algebra) isomorphism carries the convergent abstract Dynkin series termwise to the matrix Dynkin series. We put the transported bracket-submultiplicative norm on the matrix Lie algebra and then use the matrix Dynkin BCH exponential theorem explicitly assumed in the statement, with each of its hypotheses checked in that transported norm.
[/proofplan]
[step:Write Dynkin's series as a sum of nested commutators]
For non-negative integers $r$ and $s$, not both zero, let $X^rY^s$ denote the ordered word consisting of $r$ copies of $X$ followed by $s$ copies of $Y$. For a finite ordered word $W=(Z_1,\dots,Z_N)$ in the alphabet $\{X,Y\}$ with $N\geq 1$, define the right-nested commutator $C(W)\in\mathfrak g$ by
\begin{align*}
C(Z_1):=Z_1,
\end{align*}
and, for $N\geq 2$,
\begin{align*}
C(Z_1,\dots,Z_N):=[Z_1,C(Z_2,\dots,Z_N)].
\end{align*}
This is precisely the Dynkin Baker--Campbell--Hausdorff series specified in the theorem statement.
[/step]
[step:Bound each nested commutator by the product of the input norms]
We claim that for every word $W=(Z_1,\dots,Z_N)$ in $\{X,Y\}$,
\begin{align*}
\|C(W)\|_{\mathfrak g}\leq \prod_{j=1}^{N}\|Z_j\|_{\mathfrak g}.
\end{align*}
For $N=1$ this is equality. If $N\geq 2$ and the assertion is known for words of length $N-1$, then the bracket inequality gives
\begin{align*}
\|C(Z_1,\dots,Z_N)\|_{\mathfrak g}
=\|[Z_1,C(Z_2,\dots,Z_N)]\|_{\mathfrak g}
\leq \|Z_1\|_{\mathfrak g}\|C(Z_2,\dots,Z_N)\|_{\mathfrak g}.
\end{align*}
Using the induction hypothesis on $(Z_2,\dots,Z_N)$ gives
\begin{align*}
\|C(Z_1,\dots,Z_N)\|_{\mathfrak g}
\leq \prod_{j=1}^{N}\|Z_j\|_{\mathfrak g}.
\end{align*}
[guided]
The only analytic input in the convergence argument is the assumed estimate
\begin{align*}
\|[A,B]\|_{\mathfrak g}\leq \|A\|_{\mathfrak g}\|B\|_{\mathfrak g}.
\end{align*}
We need to know that this estimate propagates through iterated commutators. Let $W=(Z_1,\dots,Z_N)$ be a word whose entries are each either $X$ or $Y$. The nested commutator is defined recursively by first bracketing everything to the right, then bracketing with $Z_1$:
\begin{align*}
C(Z_1,\dots,Z_N)=[Z_1,C(Z_2,\dots,Z_N)].
\end{align*}
For $N=1$, the desired estimate says $\|Z_1\|_{\mathfrak g}\leq \|Z_1\|_{\mathfrak g}$, so it holds.
Assume it has been proved for words of length $N-1$. Applying the bracket estimate to the two elements $Z_1$ and $C(Z_2,\dots,Z_N)$ gives
\begin{align*}
\|C(Z_1,\dots,Z_N)\|_{\mathfrak g}
\leq \|Z_1\|_{\mathfrak g}\|C(Z_2,\dots,Z_N)\|_{\mathfrak g}.
\end{align*}
The induction hypothesis bounds the second factor:
\begin{align*}
\|C(Z_2,\dots,Z_N)\|_{\mathfrak g}
\leq \prod_{j=2}^{N}\|Z_j\|_{\mathfrak g}.
\end{align*}
Multiplying these two inequalities yields
\begin{align*}
\|C(Z_1,\dots,Z_N)\|_{\mathfrak g}
\leq \prod_{j=1}^{N}\|Z_j\|_{\mathfrak g}.
\end{align*}
This is the point where the Lie-algebraic problem becomes a scalar convergence problem: every commutator term is bounded by the same product one would get in a non-commutative [power series](/page/Power%20Series) with variables of sizes $\|X\|_{\mathfrak g}$ and $\|Y\|_{\mathfrak g}$.
[/guided]
[/step]
[step:Apply Dynkin's scalar majorant on the domain $\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2$]
Set
\begin{align*}
a:=\|X\|_{\mathfrak g},\qquad b:=\|Y\|_{\mathfrak g}.
\end{align*}
The estimate from the preceding step gives an absolute norm bound for each Dynkin summand. For each pair $(r_i,s_i)$, the word $X^{r_i}Y^{s_i}$ contributes the scalar factor $a^{r_i}b^{s_i}/(r_i!s_i!)$. Since the extra denominator $r_1+s_1+\cdots+r_m+s_m$ is at least $1$, the total absolute norm of the Dynkin series for $X$ and $Y$ is bounded by
\begin{align*}
\sum_{m=1}^{\infty}\frac{1}{m}\left(\sum_{\substack{r,s\geq 0, r+s>0}}\frac{a^r b^s}{r!s!}\right)^m.
\end{align*}
Using the exponential series in the two scalar variables $a$ and $b$, the inner scalar sum is
\begin{align*}
\sum_{\substack{r,s\geq 0, r+s>0}}\frac{a^r b^s}{r!s!}=e^{a+b}-1.
\end{align*}
Hence the total absolute norm is bounded by
\begin{align*}
\sum_{m=1}^{\infty}\frac{1}{m}(e^{a+b}-1)^m.
\end{align*}
This geometric-logarithmic series converges exactly when $e^{a+b}-1<1$, equivalently when $a+b<\log 2$. Under the theorem's hypothesis,
\begin{align*}
\sum_{m=1}^{\infty}\frac{1}{m}(e^{a+b}-1)^m
=-\log(2-e^{a+b})<\infty.
\end{align*}
The displayed scalar majorant is finite, so the series of norms of the Dynkin summands is finite. Since $\mathfrak g$ is finite-dimensional, it is complete for the norm $\|\cdot\|_{\mathfrak g}$; hence absolute convergence implies convergence in $\mathfrak g$. Therefore the Dynkin BCH series converges absolutely in the finite-dimensional normed space $\mathfrak g$.
[guided]
The preceding commutator estimate has reduced the problem to a scalar majorant. With
\begin{align*}
a:=\|X\|_{\mathfrak g},\qquad b:=\|Y\|_{\mathfrak g},
\end{align*}
each occurrence of $X$ in a nested commutator contributes at most a factor $a$, and each occurrence of $Y$ contributes at most a factor $b$. For a fixed block $X^rY^s$, this gives the scalar contribution $a^r b^s/(r!s!)$. The denominator $r_1+s_1+\cdots+r_m+s_m$ in Dynkin's formula is at least $1$, so taking absolute values in the full $m$-block part of the series gives the bound
\begin{align*}
\frac{1}{m}\left(\sum_{\substack{r,s\geq 0, r+s>0}}\frac{a^r b^s}{r!s!}\right)^m.
\end{align*}
The scalar sum is the exponential series in two variables with the constant term removed:
\begin{align*}
\sum_{\substack{r,s\geq 0, r+s>0}}\frac{a^r b^s}{r!s!}=e^{a+b}-1.
\end{align*}
Thus the total absolute norm of the Dynkin BCH series is bounded by
\begin{align*}
\sum_{m=1}^{\infty}\frac{1}{m}(e^{a+b}-1)^m.
\end{align*}
This is the power series for $-\log(1-z)$ with $z=e^{a+b}-1$. It converges precisely when $|z|<1$. Since $a+b\geq 0$, this condition is the same as $e^{a+b}-1<1$, which is equivalent to $a+b<\log 2$. The hypothesis of the theorem gives that inequality, and therefore
\begin{align*}
\sum_{m=1}^{\infty}\frac{1}{m}(e^{a+b}-1)^m
=-\log(2-e^{a+b})<\infty.
\end{align*}
Because the series of norms is finite and $\mathfrak g$ is finite-dimensional, $\mathfrak g$ is complete under $\|\cdot\|_{\mathfrak g}$. Thus the absolutely summable Dynkin series converges in $\mathfrak g$.
[/guided]
[/step]
[step:Transport the norm to the matrix Lie algebra and apply the matrix Dynkin BCH theorem]
Assume now that $n\in\mathbb N$, that $G\leq GL(n,\mathbb F)$ is a matrix Lie group with Lie algebra $\mathfrak h\subset M(n,\mathbb F)$, and that $\Phi:\mathfrak g\to\mathfrak h$ is the Lie algebra isomorphism from the statement. Define the transported norm $\|\cdot\|_{\Phi}$ on $\mathfrak h$ by
\begin{align*}
\|A\|_{\Phi}:=\|\Phi^{-1}(A)\|_{\mathfrak g}
\end{align*}
for $A\in\mathfrak h$. Since $\Phi$ is a Lie algebra isomorphism, for all $A,B\in\mathfrak h$ we have
\begin{align*}
\|[A,B]\|_{\Phi}
=\|[\Phi^{-1}(A),\Phi^{-1}(B)]\|_{\mathfrak g}
\leq \|\Phi^{-1}(A)\|_{\mathfrak g}\|\Phi^{-1}(B)\|_{\mathfrak g}
=\|A\|_{\Phi}\|B\|_{\Phi}.
\end{align*}
Also,
\begin{align*}
\|\Phi(X)\|_{\Phi}+\|\Phi(Y)\|_{\Phi}
=\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2.
\end{align*}
Thus the hypotheses of the matrix Dynkin BCH exponential theorem assumed in the statement are satisfied for the matrix Lie algebra $\mathfrak h$ with the norm $\|\cdot\|_{\Phi}$: $G$ is a matrix Lie group, $\mathfrak h$ is its matrix Lie algebra, the transported norm is bracket-submultiplicative, and the norm sum of $\Phi(X)$ and $\Phi(Y)$ is less than $\log 2$. We invoke exactly that theorem: for such $A,B\in\mathfrak h$, the matrix Dynkin BCH series converges absolutely and satisfies
\begin{align*}
\exp_G(A)\exp_G(B)=\exp_G(\operatorname{BCH}_{\mathfrak h}(A,B)),
\end{align*}
where $\operatorname{BCH}_{\mathfrak h}(A,B)$ is the matrix Dynkin BCH series computed using the commutator bracket in $\mathfrak h$.
Because $\Phi$ preserves brackets, an induction on word length gives
\begin{align*}
\Phi(C(Z_1,\dots,Z_N))=C(\Phi(Z_1),\dots,\Phi(Z_N))
\end{align*}
for every word $(Z_1,\dots,Z_N)$ in $\{X,Y\}$. Since $\mathfrak g$ and $\mathfrak h$ are finite-dimensional, the [linear map](/page/Linear%20Map) $\Phi:\mathfrak g\to\mathfrak h$ is continuous. Applying this continuous linear map termwise to the absolutely convergent Dynkin series therefore gives
\begin{align*}
\Phi(\operatorname{BCH}(X,Y))=\operatorname{BCH}_{\mathfrak h}(\Phi(X),\Phi(Y)).
\end{align*}
The matrix Dynkin BCH exponential theorem with $A=\Phi(X)$ and $B=\Phi(Y)$ now yields
\begin{align*}
\exp_G(\Phi(X))\exp_G(\Phi(Y))=\exp_G(\Phi(\operatorname{BCH}(X,Y))).
\end{align*}
This is the required matrix-group identity.
[guided]
The norm appearing in the theorem is a norm on the abstract Lie algebra $\mathfrak g$, not a matrix norm on $M(n,\mathbb F)$. To apply a matrix BCH result with the same numerical bound, we first move this norm to the matrix Lie algebra. Define
\begin{align*}
\|A\|_{\Phi}:=\|\Phi^{-1}(A)\|_{\mathfrak g}
\end{align*}
for $A\in\mathfrak h$. This is a norm because $\Phi:\mathfrak g\to\mathfrak h$ is a vector-space isomorphism.
We must check the bracket-submultiplicative hypothesis for this transported norm. Let $A,B\in\mathfrak h$. Since $\Phi$ is a Lie algebra isomorphism, it preserves brackets, so
\begin{align*}
\Phi^{-1}([A,B])=[\Phi^{-1}(A),\Phi^{-1}(B)].
\end{align*}
Therefore
\begin{align*}
\|[A,B]\|_{\Phi}
=\|[\Phi^{-1}(A),\Phi^{-1}(B)]\|_{\mathfrak g}
\leq \|\Phi^{-1}(A)\|_{\mathfrak g}\|\Phi^{-1}(B)\|_{\mathfrak g}
=\|A\|_{\Phi}\|B\|_{\Phi}.
\end{align*}
The smallness hypothesis is also transported exactly:
\begin{align*}
\|\Phi(X)\|_{\Phi}+\|\Phi(Y)\|_{\Phi}
=\|X\|_{\mathfrak g}+\|Y\|_{\mathfrak g}<\log 2.
\end{align*}
Thus the matrix Dynkin BCH exponential theorem assumed in the statement applies to the matrix Lie algebra $\mathfrak h$ with the transported norm $\|\cdot\|_{\Phi}$. Its hypotheses have now all been checked: $G$ is a matrix Lie group, $\mathfrak h$ is its Lie algebra, $\|\cdot\|_{\Phi}$ satisfies the bracket-submultiplicative estimate, and the norm sum is less than $\log 2$. Its conclusion is that the matrix Dynkin BCH series converges absolutely and satisfies
\begin{align*}
\exp_G(\Phi(X))\exp_G(\Phi(Y))
=\exp_G(\operatorname{BCH}_{\mathfrak h}(\Phi(X),\Phi(Y))).
\end{align*}
It remains to identify the matrix BCH term with the image under $\Phi$ of the abstract BCH term. For a word $(Z_1,\dots,Z_N)$ in $\{X,Y\}$, bracket preservation gives by induction on $N$ that
\begin{align*}
\Phi(C(Z_1,\dots,Z_N))=C(\Phi(Z_1),\dots,\Phi(Z_N)).
\end{align*}
The coefficients in Dynkin's formula are scalar, and the Dynkin series is absolutely convergent. Since $\mathfrak g$ and $\mathfrak h$ are finite-dimensional, every linear map between them is continuous; in particular $\Phi$ is continuous. Therefore applying $\Phi$ termwise to the convergent series is legitimate. Hence
\begin{align*}
\Phi(\operatorname{BCH}(X,Y))=\operatorname{BCH}_{\mathfrak h}(\Phi(X),\Phi(Y)).
\end{align*}
Substituting this identity into the matrix BCH exponential identity gives
\begin{align*}
\exp_G(\Phi(X))\exp_G(\Phi(Y))=\exp_G(\Phi(\operatorname{BCH}(X,Y))).
\end{align*}
[/guided]
[/step]
