[proofplan] The definition of $\mathfrak h$ says precisely that the one-parameter subgroup generated by $X$ remains inside the closed subgroup $H$. Scalar closure follows by reparametrising this one-parameter subgroup. Addition is obtained from the matrix Trotter product formula, because each finite approximating product lies in $H$ and closedness of $H$ passes the limit back into $H$. Closure under brackets is obtained similarly from the matrix commutator product formula, with negative parameters handled by replacing one generator by its negative. [/proofplan] [step:Record the matrix product limits used in the proof] We use the following two standard product-limit formulas for complex matrices, both with convergence in the usual topology of the [matrix space](/page/Matrix%20Space) $M(n,\mathbb C)$ declared in the theorem statement. For all $A,B\in M(n,\mathbb C)$ and all $t\in\mathbb R$, the matrix Trotter product formula gives \begin{align*} \exp(t(A+B))=\lim_{k\to\infty}\left(\exp\left(\frac{tA}{k}\right)\exp\left(\frac{tB}{k}\right)\right)^k. \end{align*} For all $A,B\in M(n,\mathbb C)$ and all $t\ge 0$, the matrix commutator product formula gives \begin{align*} \exp(t[A,B])=\lim_{k\to\infty}\left(\exp\left(\sqrt{\frac{t}{k}}A\right)\exp\left(\sqrt{\frac{t}{k}}B\right)\exp\left(-\sqrt{\frac{t}{k}}A\right)\exp\left(-\sqrt{\frac{t}{k}}B\right)\right)^k. \end{align*} Here $[A,B]:=AB-BA$ denotes the matrix commutator. Since $H$ is closed in $G$ and $G$ has the [subspace topology](/page/Subspace%20Topology) inherited from $M(n,\mathbb C)$, any sequence in $H$ that converges in $M(n,\mathbb C)$ to an element of $G$ has its limit in $H$. [/step] [step:Show that $\mathfrak h$ contains zero and is closed under real scalar multiplication] For every $t\in\mathbb R$, \begin{align*} \exp(t0)=I. \end{align*} Since $H\le G$, the identity matrix $I$ belongs to $H$. Hence $0\in\mathfrak h$. Let $X\in\mathfrak h$ and let $a\in\mathbb R$. Since $\mathfrak g$ is a real [vector space](/page/Vector%20Space), $aX\in\mathfrak g$. For every $t\in\mathbb R$, \begin{align*} \exp(t(aX))=\exp((at)X). \end{align*} Since $at\in\mathbb R$ and $X\in\mathfrak h$, the right-hand side belongs to $H$. Therefore $aX\in\mathfrak h$. [/step] [step:Use the Trotter formula to prove closure under addition] Let $X,Y\in\mathfrak h$. We prove that $X+Y\in\mathfrak h$. Fix $t\in\mathbb R$ and, for each $k\in\mathbb N$, define \begin{align*} P_k(t):=\left(\exp\left(\frac{tX}{k}\right)\exp\left(\frac{tY}{k}\right)\right)^k\in G. \end{align*} Because $X,Y\in\mathfrak h$, both $\exp(tX/k)$ and $\exp(tY/k)$ belong to $H$. Since $H$ is a subgroup, $P_k(t)\in H$ for every $k\in\mathbb N$. By the matrix Trotter product formula, \begin{align*} P_k(t)\to \exp(t(X+Y)) \end{align*} in $M(n,\mathbb C)$. Also $X+Y\in\mathfrak g$ because $\mathfrak g$ is a real vector space, so $\exp(t(X+Y))\in G$. Since $H$ is closed in $G$, the limit belongs to $H$. Thus $\exp(t(X+Y))\in H$ for every $t\in\mathbb R$, and hence $X+Y\in\mathfrak h$. [guided] We want to prove that the one-parameter subgroup generated by $X+Y$ stays in $H$. The difficulty is that matrix exponentials do not generally satisfy $\exp(t(X+Y))=\exp(tX)\exp(tY)$ when $X$ and $Y$ do not commute. The Trotter product formula replaces this false identity by a true limiting identity: \begin{align*} \exp(t(X+Y))=\lim_{k\to\infty}\left(\exp\left(\frac{tX}{k}\right)\exp\left(\frac{tY}{k}\right)\right)^k. \end{align*} Fix $t\in\mathbb R$. For each $k\in\mathbb N$, define the approximating matrix \begin{align*} P_k(t):=\left(\exp\left(\frac{tX}{k}\right)\exp\left(\frac{tY}{k}\right)\right)^k. \end{align*} Since $X\in\mathfrak h$, the defining property of $\mathfrak h$ gives $\exp((t/k)X)\in H$. Since $Y\in\mathfrak h$, it also gives $\exp((t/k)Y)\in H$. The subgroup property of $H$ then implies that their product lies in $H$, and applying the subgroup property repeatedly gives $P_k(t)\in H$. The Trotter formula gives convergence $P_k(t)\to\exp(t(X+Y))$ in the matrix topology. We also know $X+Y\in\mathfrak g$ because $\mathfrak g$ is a real vector space, so $\exp(t(X+Y))$ is an element of $G$. Now the closedness of $H$ is exactly the hypothesis that lets us pass from approximants in $H$ to their limit: since $H$ is closed in $G$, the limit $\exp(t(X+Y))$ belongs to $H$. Because $t\in\mathbb R$ was arbitrary, $\exp(t(X+Y))\in H$ for every $t\in\mathbb R$, which is precisely $X+Y\in\mathfrak h$. [/guided] [/step] [step:Use the commutator formula to prove closure under brackets] Let $X,Y\in\mathfrak h$. We prove that $[X,Y]\in\mathfrak h$. First fix $t\ge 0$. For each $k\in\mathbb N$, define \begin{align*} C_k(t):=\left(\exp\left(\sqrt{\frac{t}{k}}X\right)\exp\left(\sqrt{\frac{t}{k}}Y\right)\exp\left(-\sqrt{\frac{t}{k}}X\right)\exp\left(-\sqrt{\frac{t}{k}}Y\right)\right)^k\in G. \end{align*} Since $X,Y\in\mathfrak h$, all four factors inside the parentheses belong to $H$. Since $H$ is a subgroup, $C_k(t)\in H$ for every $k\in\mathbb N$. By the matrix commutator product formula, \begin{align*} C_k(t)\to \exp(t[X,Y]) \end{align*} in $M(n,\mathbb C)$. Since $[X,Y]\in\mathfrak g$ because $\mathfrak g$ is closed under its Lie bracket, the limit $\exp(t[X,Y])$ belongs to $G$. Closedness of $H$ in $G$ gives $\exp(t[X,Y])\in H$ for every $t\ge 0$. Now let $t<0$. Put $s:=-t>0$. By scalar closure already proved, $-X\in\mathfrak h$. Applying the nonnegative case to $-X$ and $Y$ gives \begin{align*} \exp(s[-X,Y])\in H. \end{align*} Since $[-X,Y]=-[X,Y]$, this is \begin{align*} \exp(t[X,Y])\in H. \end{align*} Therefore $\exp(t[X,Y])\in H$ for every $t\in\mathbb R$, so $[X,Y]\in\mathfrak h$. [/step] [step:Conclude that $\mathfrak h$ is a Lie subalgebra of $\mathfrak g$] The set $\mathfrak h$ is a subset of $\mathfrak g$ by definition. The preceding steps show that $\mathfrak h$ contains $0$, is closed under real scalar multiplication, and is closed under addition; hence $\mathfrak h$ is a real vector subspace of $\mathfrak g$. The commutator step shows that $[X,Y]\in\mathfrak h$ whenever $X,Y\in\mathfrak h$. Therefore $\mathfrak h$ is a real Lie subalgebra of $\mathfrak g$. [/step]