[proofplan] Define the infinitesimal subgroup $\mathfrak h$ as the set of all directions in $\mathfrak g$ whose full exponential one-parameter subgroup lies in $H$. The key point is local: after choosing a complement $\mathfrak m$ to $\mathfrak h$, adapted exponential coordinates write every element near the identity uniquely as $\exp(X)\exp(Y)$ with $X\in\mathfrak h$ and $Y\in\mathfrak m$. The no-small-transverse-elements theorem forces $Y=0$ for elements of $H$ sufficiently near the identity, so near the identity $H$ is exactly an exponential slice from $\mathfrak h$. Translating this slice by elements of $H$ gives embedded charts on all of $H$, and the group operations are smooth because they are restrictions of the smooth group operations on $G$. [/proofplan] [step:Define the infinitesimal subgroup and choose a transverse complement] Define \begin{align*} \mathfrak h:=\{X\in\mathfrak g:\exp(tX)\in H\text{ for all }t\in\mathbb R\}. \end{align*} Since $H$ is a closed subgroup of the matrix Lie group $G$, [citetheorem:8810] implies that $\mathfrak h$ is a Lie subalgebra of $\mathfrak g$; in particular, $\mathfrak h$ is a real vector subspace of $\mathfrak g$. Because $\mathfrak g$ is finite-dimensional over $\mathbb R$, choose a real vector subspace $\mathfrak m\subset\mathfrak g$ such that \begin{align*} \mathfrak g=\mathfrak h\oplus\mathfrak m. \end{align*} This means that every $Z\in\mathfrak g$ has a unique decomposition $Z=X+Y$ with $X\in\mathfrak h$ and $Y\in\mathfrak m$. [guided] We first isolate the candidate [Lie algebra](/page/Lie%20Algebra) of the closed subgroup. Define \begin{align*} \mathfrak h:=\{X\in\mathfrak g:\exp(tX)\in H\text{ for all }t\in\mathbb R\}. \end{align*} This definition says that $X$ belongs to $\mathfrak h$ exactly when the whole one-parameter subgroup generated by $X$ stays inside $H$. The hypothesis needed for [citetheorem:8810] is precisely that $G$ is a matrix Lie group and that $H\le G$ is a closed subgroup. These hypotheses are part of the theorem statement, so the result applies and gives that $\mathfrak h$ is a Lie subalgebra of $\mathfrak g$. In particular, $\mathfrak h$ is a real vector subspace of $\mathfrak g$. The next move is to separate directions tangent to $H$ from directions transverse to $H$. Since $\mathfrak g$ is finite-dimensional as a real [vector space](/page/Vector%20Space), every subspace has a vector-space complement. Choose a real vector subspace $\mathfrak m\subset\mathfrak g$ satisfying \begin{align*} \mathfrak g=\mathfrak h\oplus\mathfrak m. \end{align*} Thus every $Z\in\mathfrak g$ can be written uniquely as $Z=X+Y$, where $X\in\mathfrak h$ and $Y\in\mathfrak m$. The proof will show that, near the identity, the elements of $H$ have no nonzero $\mathfrak m$-component. [/guided] [/step] [step:Use adapted exponential coordinates near the identity] The hypotheses of [citetheorem:8811] are satisfied: $G$ is a matrix Lie group, $\mathfrak h\subset\mathfrak g$ is a real vector subspace, and $\mathfrak g=\mathfrak h\oplus\mathfrak m$ by construction. Hence there exist open neighbourhoods $U_{\mathfrak h}\subset\mathfrak h$ of $0$, $U_{\mathfrak m}\subset\mathfrak m$ of $0$, and $U_G\subset G$ of $e$, such that the map \begin{align*} \Phi:U_{\mathfrak h}\times U_{\mathfrak m}\to U_G \end{align*} defined by \begin{align*} \Phi(X,Y)=\exp(X)\exp(Y) \end{align*} is a diffeomorphism. The hypotheses of [citetheorem:8812] are also satisfied: $G$ is a matrix Lie group, $H\le G$ is closed, $\mathfrak h$ is the infinitesimal subgroup just defined, and $\mathfrak m$ is a complement with $\mathfrak g=\mathfrak h\oplus\mathfrak m$. Therefore, after shrinking $U_{\mathfrak m}$ if necessary, we may also assume that \begin{align*} H\cap \exp(U_{\mathfrak m})=\{e\}. \end{align*} After replacing $U_G$ by $\Phi(U_{\mathfrak h}\times U_{\mathfrak m})$ for the shrunk neighbourhoods, the map $\Phi$ remains a diffeomorphism onto an open neighbourhood of $e$ in $G$. [guided] We now choose coordinates near the identity that are adapted to the decomposition $\mathfrak g=\mathfrak h\oplus\mathfrak m$. The adapted-coordinate theorem [citetheorem:8811] applies because $G$ is a matrix Lie group, because $\mathfrak h$ is a vector subspace of $\mathfrak g$, and because $\mathfrak m$ was chosen so that every element of $\mathfrak g$ decomposes uniquely into an $\mathfrak h$-part and an $\mathfrak m$-part. Thus there are open neighbourhoods $U_{\mathfrak h}\subset\mathfrak h$, $U_{\mathfrak m}\subset\mathfrak m$, and $U_G\subset G$ of $0$, $0$, and $e$, respectively, for which \begin{align*} \Phi:U_{\mathfrak h}\times U_{\mathfrak m}\to U_G \end{align*} defined by \begin{align*} \Phi(X,Y)=\exp(X)\exp(Y) \end{align*} is a diffeomorphism. This gives each element of $U_G$ a unique pair of local coordinates $(X,Y)$, with $X$ tangent to the candidate subgroup and $Y$ transverse to it. Next we use the closedness of $H$ through [citetheorem:8812]. That result requires exactly the data now in place: a matrix Lie group $G$, a closed subgroup $H\le G$, the infinitesimal subgroup $\mathfrak h$, and a complement $\mathfrak m$ satisfying $\mathfrak g=\mathfrak h\oplus\mathfrak m$. It gives a neighbourhood of $0$ in $\mathfrak m$ on which no nonidentity exponential can lie in $H$. Shrinking $U_{\mathfrak m}$ to such a neighbourhood, we have \begin{align*} H\cap \exp(U_{\mathfrak m})=\{e\}. \end{align*} After this shrinkage, we replace $U_G$ by $\Phi(U_{\mathfrak h}\times U_{\mathfrak m})$. Since $\Phi$ is still a diffeomorphism on the smaller product neighbourhood, this new $U_G$ is again an open neighbourhood of $e$ in $G$. [/guided] [/step] [step:Show that the closed subgroup has no transverse coordinate near the identity] We claim that \begin{align*} H\cap U_G=\Phi(U_{\mathfrak h}\times\{0\}). \end{align*} First let $X\in U_{\mathfrak h}$. Since $X\in\mathfrak h$, the definition of $\mathfrak h$ gives $\exp(tX)\in H$ for every $t\in\mathbb R$, hence $\exp(X)\in H$. Therefore \begin{align*} \Phi(X,0)=\exp(X)\in H\cap U_G. \end{align*} This proves \begin{align*} \Phi(U_{\mathfrak h}\times\{0\})\subset H\cap U_G. \end{align*} Conversely, let $h\in H\cap U_G$. Since $\Phi$ is surjective onto $U_G$, there are unique $X\in U_{\mathfrak h}$ and $Y\in U_{\mathfrak m}$ such that \begin{align*} h=\Phi(X,Y)=\exp(X)\exp(Y). \end{align*} Because $X\in\mathfrak h$, we have $\exp(X)\in H$ and $\exp(-X)\in H$. Since $h\in H$ and $H$ is a subgroup, \begin{align*} \exp(Y)=\exp(-X)h\in H. \end{align*} Also $\exp(Y)\in\exp(U_{\mathfrak m})$, so the no-small-transverse-elements condition gives $\exp(Y)=e$. Hence \begin{align*} \Phi(0,Y)=e=\Phi(0,0). \end{align*} The injectivity of $\Phi$ on $U_{\mathfrak h}\times U_{\mathfrak m}$ implies $Y=0$. Thus $h=\Phi(X,0)$, and the reverse inclusion follows. [guided] The adapted coordinate map writes each element near $e$ in the form \begin{align*} \Phi(X,Y)=\exp(X)\exp(Y), \end{align*} where $X$ is an $\mathfrak h$-direction and $Y$ is an $\mathfrak m$-direction. We prove that an element of $H$ near $e$ must have $Y=0$. First take $X\in U_{\mathfrak h}$. Since $U_{\mathfrak h}\subset\mathfrak h$, the definition of $\mathfrak h$ gives $\exp(tX)\in H$ for all $t\in\mathbb R$. Evaluating at $t=1$ gives $\exp(X)\in H$. Therefore \begin{align*} \Phi(X,0)=\exp(X)\exp(0)=\exp(X)\in H\cap U_G. \end{align*} So every point in the slice $\Phi(U_{\mathfrak h}\times\{0\})$ belongs to $H$. Now let $h\in H\cap U_G$. Since $\Phi:U_{\mathfrak h}\times U_{\mathfrak m}\to U_G$ is a diffeomorphism, it is in particular bijective. Hence there are unique elements $X\in U_{\mathfrak h}$ and $Y\in U_{\mathfrak m}$ such that \begin{align*} h=\Phi(X,Y)=\exp(X)\exp(Y). \end{align*} The element $X$ lies in $\mathfrak h$, so $\exp(tX)\in H$ for all real $t$. Taking $t=1$ and $t=-1$ gives $\exp(X)\in H$ and $\exp(-X)\in H$. Since $H$ is a subgroup and $h\in H$, multiplication inside $H$ gives \begin{align*} \exp(Y)=\exp(-X)h\in H. \end{align*} At the same time, $Y\in U_{\mathfrak m}$, so $\exp(Y)\in\exp(U_{\mathfrak m})$. The neighbourhood $U_{\mathfrak m}$ was chosen so that \begin{align*} H\cap \exp(U_{\mathfrak m})=\{e\}. \end{align*} Therefore $\exp(Y)=e$. It remains to convert $\exp(Y)=e$ into $Y=0$. This is where uniqueness in the adapted coordinate chart is used. Since \begin{align*} \Phi(0,Y)=\exp(0)\exp(Y)=e \end{align*} and \begin{align*} \Phi(0,0)=\exp(0)\exp(0)=e, \end{align*} injectivity of $\Phi$ on $U_{\mathfrak h}\times U_{\mathfrak m}$ implies $(0,Y)=(0,0)$, hence $Y=0$. Thus every element of $H\cap U_G$ lies in $\Phi(U_{\mathfrak h}\times\{0\})$, proving \begin{align*} H\cap U_G=\Phi(U_{\mathfrak h}\times\{0\}). \end{align*} [/guided] [/step] [step:Build the embedded manifold structure on $H$ by translating the identity chart] Define \begin{align*} S_e:=H\cap U_G=\Phi(U_{\mathfrak h}\times\{0\}). \end{align*} The map \begin{align*} \theta_e:S_e&\to U_{\mathfrak h} \end{align*} defined by \begin{align*} \theta_e(\exp(X))=X \end{align*} is well-defined because $\Phi|_{U_{\mathfrak h}\times\{0\}}$ is injective. It is a chart whose inverse is \begin{align*} \theta_e^{-1}:U_{\mathfrak h}&\to S_e \end{align*} given by \begin{align*} \theta_e^{-1}(X)=\exp(X). \end{align*} Since $\Phi$ is a diffeomorphism and $U_{\mathfrak h}\times\{0\}$ is an embedded submanifold of $U_{\mathfrak h}\times U_{\mathfrak m}$, the set $S_e$ is an embedded submanifold of $G$ near $e$ with model space $\mathfrak h$. For each $a\in H$, let $L_a:G\to G$ be the left-translation diffeomorphism defined by $L_a(g)=ag$. Define \begin{align*} S_a:=L_a(S_e)=aS_e. \end{align*} Since $S_e=H\cap U_G$ and $a\in H$, the subgroup property gives \begin{align*} S_a=a(H\cap U_G)=H\cap aU_G. \end{align*} Thus $S_a$ is a relative neighbourhood of $a$ in $H$. The map \begin{align*} \theta_a:S_a\to U_{\mathfrak h} \end{align*} defined by \begin{align*} \theta_a(a\exp(X))=X \end{align*} is a chart on $S_a$, and $S_a$ is an embedded submanifold of $G$ because it is the image of the embedded submanifold $S_e$ under the diffeomorphism $L_a$. The family of charts $\{\theta_a:S_a\to U_{\mathfrak h}\}_{a\in H}$ covers $H$, since $a\in S_a$ for every $a\in H$. On overlaps, the transition maps are restrictions of smooth transition maps between embedded submanifold charts of $G$, because both charts are obtained from the same embedded slice by smooth left translations in $G$. Hence these charts define a smooth manifold structure on $H$, compatible with the [subspace topology](/page/Subspace%20Topology) inherited from $G$, for which the inclusion $H\hookrightarrow G$ is locally the inclusion of an embedded submanifold. [guided] The identity slice gives only a chart near $e$, so we translate it to every point of $H$. For $a\in H$, the left translation map \begin{align*} L_a:G\to G \end{align*} defined by $L_a(g)=ag$ is a diffeomorphism of $G$. We set \begin{align*} S_a:=L_a(S_e)=aS_e. \end{align*} Because $S_e=H\cap U_G$ and $a\in H$, multiplication by $a$ carries $H$ onto $H$ and $U_G$ onto the open neighbourhood $aU_G$ of $a$ in $G$. Hence \begin{align*} S_a=a(H\cap U_G)=H\cap aU_G. \end{align*} So $S_a$ is not merely a subset of $H$; it is a neighbourhood of $a$ in the topology inherited from $G$. The chart on this translated slice is \begin{align*} \theta_a:S_a\to U_{\mathfrak h} \end{align*} given by \begin{align*} \theta_a(a\exp(X))=X. \end{align*} This is well-defined because the identity chart was well-defined and left translation is injective. Since $S_a=L_a(S_e)$ and $L_a$ is a diffeomorphism of $G$, each $S_a$ is an embedded submanifold of $G$ with the same model space $\mathfrak h$. The sets $S_a$ cover $H$ because $a=a e$ and $e\in S_e$, so $a\in S_a$. On an overlap $S_a\cap S_b$, both charts are obtained by restricting embedded submanifold charts of $G$ and composing with smooth left translations. Therefore their transition maps are smooth. These charts give a smooth manifold structure on $H$ compatible with the subspace topology, and in each chart the inclusion $H\hookrightarrow G$ is the local inclusion of an embedded submanifold. [/guided] [/step] [step:Restrict the smooth group operations and identify the Lie algebra] Let \begin{align*} \mu_G:G\times G&\to G \end{align*} be the multiplication map $\mu_G(g_1,g_2)=g_1g_2$, and let \begin{align*} \iota_G:G&\to G \end{align*} be the inversion map $\iota_G(g)=g^{-1}$. Since $G$ is a Lie group, both maps are smooth. Because $H\le G$ is a subgroup, the restrictions \begin{align*} \mu_H:H\times H\to H \end{align*} and \begin{align*} \iota_H:H\to H \end{align*} are well-defined. We use the embedded-submanifold smoothness criterion: if $M$ is an embedded submanifold of a smooth manifold $N$, a map $f:P\to M$ is smooth exactly when the composite $P\xrightarrow{f}M\hookrightarrow N$ is smooth, with $P$ any smooth manifold. In the embedded charts constructed above, the compositions of $\mu_H$ and $\iota_H$ with the inclusion $H\hookrightarrow G$ are respectively the restrictions of the smooth ambient maps $\mu_G$ and $\iota_G$ to $H\times H$ and $H$. Since $H\times H$ carries the product smooth structure from the embedded manifold structure on $H$, the criterion implies that $\mu_H$ and $\iota_H$ are smooth. Therefore $H$ is a Lie subgroup of $G$. It remains to identify its Lie algebra. In the identity chart, the embedded submanifold $H$ near $e$ is precisely \begin{align*} S_e=\{\exp(X):X\in U_{\mathfrak h}\}. \end{align*} The tangent space at $e$ is therefore \begin{align*} T_eH=\mathfrak h\subset T_eG=\mathfrak g, \end{align*} where the identification is the differential at $0$ of the exponential chart $X\mapsto\exp(X)$. Since [citetheorem:8785] identifies the Lie algebra of a matrix Lie group with its tangent space at the identity, we obtain \begin{align*} \operatorname{Lie}(H)=T_eH=\mathfrak h =\{X\in\mathfrak g:\exp(tX)\in H\text{ for all }t\in\mathbb R\}. \end{align*} This is the claimed formula, and the proof is complete. [guided] The multiplication and inversion on $H$ are set-theoretically inherited from $G$. Let \begin{align*} \mu_G:G\times G\to G \end{align*} be multiplication and let \begin{align*} \iota_G:G\to G \end{align*} be inversion. Since $G$ is a Lie group, both are smooth. Because $H$ is a subgroup, the restricted maps \begin{align*} \mu_H:H\times H\to H \end{align*} and \begin{align*} \iota_H:H\to H \end{align*} are well-defined. To see smoothness, use the embedded-submanifold smoothness criterion. This criterion says that, for an embedded submanifold $M\subset N$, a map $f:P\to M$ from a smooth manifold $P$ is smooth if and only if the same set map, viewed as a map $P\to N$ by composing with the inclusion $M\hookrightarrow N$, is smooth. Here $M=H$ and $N=G$. The composite of $\mu_H:H\times H\to H$ with the inclusion $H\hookrightarrow G$ is the restriction of the smooth multiplication map $\mu_G:G\times G\to G$ to the embedded submanifold $H\times H\subset G\times G$. Likewise, the composite of $\iota_H:H\to H$ with $H\hookrightarrow G$ is the restriction of the smooth inversion map $\iota_G:G\to G$ to $H$. Therefore the criterion applies to both restricted maps, so $\mu_H$ and $\iota_H$ are smooth. Hence $H$ is a Lie subgroup of $G$. Finally we compute the Lie algebra. Near $e$, the subgroup is exactly the exponential slice \begin{align*} S_e=\{\exp(X):X\in U_{\mathfrak h}\}. \end{align*} The chart inverse is $X\mapsto\exp(X)$, and the differential of this chart inverse at $0$ identifies the model space $\mathfrak h$ with the tangent space $T_eH$. Thus \begin{align*} T_eH=\mathfrak h\subset T_eG=\mathfrak g. \end{align*} By [citetheorem:8785], the Lie algebra of a matrix Lie group is its tangent space at the identity under this identification. Therefore \begin{align*} \operatorname{Lie}(H)=T_eH=\mathfrak h =\{X\in\mathfrak g:\exp(tX)\in H\text{ for all }t\in\mathbb R\}. \end{align*} This is exactly the asserted Lie algebra formula. [/guided] [/step]