[proofplan] The splitting $s$ embeds $\mathfrak k$ as a Lie subalgebra of $\mathfrak g$, while exactness identifies $\mathfrak h$ with the ideal $\ker \pi$. We first show that every element of $\mathfrak g$ has a unique decomposition as an element of $\iota(\mathfrak h)$ plus an element of $s(\mathfrak k)$. The bracket with $s(k)$ then defines an action $\rho(k)$ on $\mathfrak h$; the Jacobi identity shows that each $\rho(k)$ is a derivation and that $\rho$ is a Lie algebra homomorphism. Finally, the unique decomposition map is checked directly to preserve the semidirect product bracket. [/proofplan]

[step:Identify $\mathfrak h$ as an ideal and $s(\mathfrak k)$ as a subalgebra of $\mathfrak g$]Since the sequence is exact, $\iota:\mathfrak h \to \mathfrak g$ is injective and \begin{align*} \operatorname{im}\iota = \ker \pi. \end{align*} Because $\pi:\mathfrak g \to \mathfrak k$ is a Lie algebra homomorphism, $\ker \pi$ is an ideal of $\mathfrak g$: if $x \in \ker \pi$ and $y \in \mathfrak g$, then \begin{align*} \pi([y,x]_{\mathfrak g}) = [\pi(y),\pi(x)]_{\mathfrak k} = [\pi(y),0]_{\mathfrak k} = 0, \end{align*} so $[y,x]_{\mathfrak g} \in \ker \pi$. Hence $\iota(\mathfrak h)$ is an ideal of $\mathfrak g$. Since $s:\mathfrak k \to \mathfrak g$ is a Lie algebra homomorphism, its image $s(\mathfrak k)$ is a Lie subalgebra of $\mathfrak g$. Also $\pi \circ s = \operatorname{id}_{\mathfrak k}$ implies that $s$ is injective: if $s(k)=0$, then \begin{align*} k = (\pi \circ s)(k)=\pi(0)=0. \end{align*} Thus $s$ identifies $\mathfrak k$ with the Lie subalgebra $s(\mathfrak k) \subset \mathfrak g$.[/step]

[guided]The exact sequence gives two structural facts. First, $\iota$ embeds $\mathfrak h$ into $\mathfrak g$, because exactness at $\mathfrak h$ means $\ker \iota = 0$. Second, exactness at $\mathfrak g$ says \begin{align*} \operatorname{im}\iota = \ker \pi. \end{align*} We need $\iota(\mathfrak h)$ to be an ideal because later we will bracket an arbitrary element $s(k)$ with an element $\iota(h)$ and want the result to land back inside $\iota(\mathfrak h)$. Let $x \in \ker \pi$ and $y \in \mathfrak g$. Since $\pi$ is a Lie algebra homomorphism, \begin{align*} \pi([y,x]_{\mathfrak g}) = [\pi(y),\pi(x)]_{\mathfrak k} = [\pi(y),0]_{\mathfrak k} = 0. \end{align*} Therefore $[y,x]_{\mathfrak g} \in \ker \pi$, proving that $\ker \pi=\iota(\mathfrak h)$ is an ideal. The splitting $s:\mathfrak k \to \mathfrak g$ is also a Lie algebra homomorphism, so its image is closed under the bracket: \begin{align*} [s(k_1),s(k_2)]_{\mathfrak g} = s([k_1,k_2]_{\mathfrak k}) \end{align*} for all $k_1,k_2 \in \mathfrak k$. Hence $s(\mathfrak k)$ is a Lie subalgebra of $\mathfrak g$. Finally, $\pi \circ s=\operatorname{id}_{\mathfrak k}$ forces $s$ to be injective, because $s(k)=0$ implies \begin{align*} k=(\pi \circ s)(k)=\pi(0)=0. \end{align*} Thus $s$ realizes $\mathfrak k$ inside $\mathfrak g$ as the subalgebra $s(\mathfrak k)$.[/guided]

[step:Decompose every element of $\mathfrak g$ uniquely as $\iota(h)+s(k)$]Define the $\mathbb F$-[linear map](/page/Linear%20Map) \begin{align*} \Phi:\mathfrak h \oplus \mathfrak k &\to \mathfrak g \\ (h,k) &\mapsto \iota(h)+s(k). \end{align*} We prove that $\Phi$ is a [vector space](/page/Vector%20Space) isomorphism. Let $x \in \mathfrak g$. Define $k \in \mathfrak k$ by $k:=\pi(x)$. Then \begin{align*} \pi(x-s(k)) = \pi(x)-(\pi\circ s)(k) = k-k =0, \end{align*} so $x-s(k) \in \ker \pi=\operatorname{im}\iota$. Hence there exists $h \in \mathfrak h$ such that \begin{align*} x-s(k)=\iota(h), \end{align*} and therefore $x=\iota(h)+s(k)$. Thus $\Phi$ is surjective. For injectivity, suppose $\Phi(h,k)=0$. Applying $\pi$ gives \begin{align*} 0 = \pi(\iota(h)+s(k)) = \pi(\iota(h))+(\pi\circ s)(k) = 0+k = k. \end{align*} Thus $k=0$, and then $\iota(h)=0$. Since $\iota$ is injective, $h=0$. Hence $\Phi$ is injective.[/step]

[guided]The desired isomorphism should send a pair $(h,k)$ to the sum of the corresponding pieces in $\mathfrak g$. Define \begin{align*} \Phi:\mathfrak h \oplus \mathfrak k &\to \mathfrak g \\ (h,k) &\mapsto \iota(h)+s(k). \end{align*} At this stage $\Phi$ is only a linear map. We first prove that it is a vector space isomorphism; the bracket computation comes later. To prove surjectivity, take an arbitrary $x \in \mathfrak g$. The only possible $\mathfrak k$-component is forced by applying $\pi$, so define \begin{align*} k:=\pi(x) \in \mathfrak k. \end{align*} Subtract the lifted element $s(k)$ from $x$. Since $\pi \circ s=\operatorname{id}_{\mathfrak k}$, \begin{align*} \pi(x-s(k)) = \pi(x)-(\pi\circ s)(k) = k-k =0. \end{align*} Thus $x-s(k) \in \ker \pi$. Exactness says $\ker \pi=\operatorname{im}\iota$, so there is some $h \in \mathfrak h$ such that \begin{align*} x-s(k)=\iota(h). \end{align*} Therefore $x=\iota(h)+s(k)$, proving that $\Phi$ is surjective. For uniqueness, suppose \begin{align*} \Phi(h,k)=\iota(h)+s(k)=0. \end{align*} Apply $\pi$ to isolate the $\mathfrak k$-component: \begin{align*} 0 = \pi(\iota(h)+s(k)) = \pi(\iota(h))+(\pi\circ s)(k) = 0+k = k. \end{align*} With $k=0$, the equation becomes $\iota(h)=0$. Exactness gives injectivity of $\iota$, so $h=0$. Thus the representation $x=\iota(h)+s(k)$ is unique, and $\Phi$ is a vector space isomorphism.[/guided]

[step:Define the action of $\mathfrak k$ on $\mathfrak h$ by bracketing with the splitting] For each $k \in \mathfrak k$, define a map \begin{align*} \rho(k):\mathfrak h &\to \mathfrak h \\ h &\mapsto \iota^{-1}([s(k),\iota(h)]_{\mathfrak g}). \end{align*} This is well-defined because $\iota(\mathfrak h)=\ker \pi$ is an ideal of $\mathfrak g$, so $[s(k),\iota(h)]_{\mathfrak g} \in \iota(\mathfrak h)$, and because $\iota:\mathfrak h \to \iota(\mathfrak h)$ is a vector space isomorphism. The map $\rho(k)$ is $\mathbb F$-linear. Indeed, for $a,b \in \mathbb F$ and $h_1,h_2 \in \mathfrak h$, \begin{align*} \iota(\rho(k)(a h_1+b h_2)) &= [s(k),\iota(a h_1+b h_2)]_{\mathfrak g} \\ &= [s(k),a\iota(h_1)+b\iota(h_2)]_{\mathfrak g} \\ &= a[s(k),\iota(h_1)]_{\mathfrak g} + b[s(k),\iota(h_2)]_{\mathfrak g} \\ &= \iota(a\rho(k)(h_1)+b\rho(k)(h_2)). \end{align*} Since $\iota$ is injective, \begin{align*} \rho(k)(a h_1+b h_2)=a\rho(k)(h_1)+b\rho(k)(h_2). \end{align*} Let $\operatorname{End}_{\mathbb F}(\mathfrak h)$ denote the vector space of $\mathbb F$-linear maps from $\mathfrak h$ to itself. Also $\rho:\mathfrak k \to \operatorname{End}_{\mathbb F}(\mathfrak h)$ is $\mathbb F$-linear. For $a,b \in \mathbb F$, $k_1,k_2 \in \mathfrak k$, and $h \in \mathfrak h$, \begin{align*} \iota(\rho(a k_1+b k_2)(h)) &= [s(a k_1+b k_2),\iota(h)]_{\mathfrak g} \\ &= [a s(k_1)+b s(k_2),\iota(h)]_{\mathfrak g} \\ &= a[s(k_1),\iota(h)]_{\mathfrak g} + b[s(k_2),\iota(h)]_{\mathfrak g} \\ &= \iota(a\rho(k_1)(h)+b\rho(k_2)(h)). \end{align*} Injectivity of $\iota$ gives \begin{align*} \rho(a k_1+b k_2)=a\rho(k_1)+b\rho(k_2). \end{align*} [/step]

[step:Use the Jacobi identity to prove that each $\rho(k)$ is a derivation]Fix $k \in \mathfrak k$. We prove that $\rho(k) \in \operatorname{Der}(\mathfrak h)$, where $\operatorname{Der}(\mathfrak h)$ denotes the Lie algebra of $\mathbb F$-linear derivations of $\mathfrak h$ with bracket the commutator. Let $h_1,h_2 \in \mathfrak h$. Since $\iota$ is a Lie algebra homomorphism, \begin{align*} \iota(\rho(k)([h_1,h_2]_{\mathfrak h})) &= [s(k),\iota([h_1,h_2]_{\mathfrak h})]_{\mathfrak g} \\ &= [s(k),[\iota(h_1),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} By the Jacobi identity in $\mathfrak g$, written in derivation form, \begin{align*} [s(k),[\iota(h_1),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g} &= [[s(k),\iota(h_1)]_{\mathfrak g},\iota(h_2)]_{\mathfrak g} + [\iota(h_1),[s(k),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} Using the definition of $\rho(k)$ and the fact that $\iota$ is a Lie algebra homomorphism, this becomes \begin{align*} \iota(\rho(k)([h_1,h_2]_{\mathfrak h})) &= [\iota(\rho(k)(h_1)),\iota(h_2)]_{\mathfrak g} + [\iota(h_1),\iota(\rho(k)(h_2))]_{\mathfrak g} \\ &= \iota([\rho(k)(h_1),h_2]_{\mathfrak h}) + \iota([h_1,\rho(k)(h_2)]_{\mathfrak h}) \\ &= \iota([\rho(k)(h_1),h_2]_{\mathfrak h} + [h_1,\rho(k)(h_2)]_{\mathfrak h}). \end{align*} Since $\iota$ is injective, \begin{align*} \rho(k)([h_1,h_2]_{\mathfrak h}) = [\rho(k)(h_1),h_2]_{\mathfrak h} + [h_1,\rho(k)(h_2)]_{\mathfrak h}. \end{align*} Thus $\rho(k)$ is a derivation of $\mathfrak h$.[/step]

[guided]A derivation of $\mathfrak h$ is an $\mathbb F$-linear map $D:\mathfrak h \to \mathfrak h$ satisfying the Leibniz rule \begin{align*} D([h_1,h_2]_{\mathfrak h}) = [D(h_1),h_2]_{\mathfrak h} + [h_1,D(h_2)]_{\mathfrak h} \end{align*} for all $h_1,h_2 \in \mathfrak h$. We already proved that $\rho(k)$ is linear, so it remains to prove this identity for $D=\rho(k)$. Fix $k \in \mathfrak k$ and $h_1,h_2 \in \mathfrak h$. Since $\iota$ is a Lie algebra homomorphism, \begin{align*} \iota([h_1,h_2]_{\mathfrak h}) = [\iota(h_1),\iota(h_2)]_{\mathfrak g}. \end{align*} Therefore, by the definition of $\rho(k)$, \begin{align*} \iota(\rho(k)([h_1,h_2]_{\mathfrak h})) &= [s(k),\iota([h_1,h_2]_{\mathfrak h})]_{\mathfrak g} \\ &= [s(k),[\iota(h_1),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} Now apply the Jacobi identity in the form that says the adjoint map $[a,\cdot]$ acts as a derivation: \begin{align*} [a,[b,c]]=[[a,b],c]+[b,[a,c]]. \end{align*} Here we take $a=s(k)$, $b=\iota(h_1)$, and $c=\iota(h_2)$. This gives \begin{align*} [s(k),[\iota(h_1),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g} &= [[s(k),\iota(h_1)]_{\mathfrak g},\iota(h_2)]_{\mathfrak g} + [\iota(h_1),[s(k),\iota(h_2)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} By definition of $\rho(k)$, \begin{align*} [s(k),\iota(h_i)]_{\mathfrak g}=\iota(\rho(k)(h_i)) \end{align*} for $i \in \{1,2\}$. Substituting this into the previous identity and using that $\iota$ preserves brackets, we obtain \begin{align*} \iota(\rho(k)([h_1,h_2]_{\mathfrak h})) &= [\iota(\rho(k)(h_1)),\iota(h_2)]_{\mathfrak g} + [\iota(h_1),\iota(\rho(k)(h_2))]_{\mathfrak g} \\ &= \iota([\rho(k)(h_1),h_2]_{\mathfrak h}) + \iota([h_1,\rho(k)(h_2)]_{\mathfrak h}) \\ &= \iota([\rho(k)(h_1),h_2]_{\mathfrak h} + [h_1,\rho(k)(h_2)]_{\mathfrak h}). \end{align*} Injectivity of $\iota$ lets us cancel $\iota$ from both sides, so \begin{align*} \rho(k)([h_1,h_2]_{\mathfrak h}) = [\rho(k)(h_1),h_2]_{\mathfrak h} + [h_1,\rho(k)(h_2)]_{\mathfrak h}. \end{align*} Thus $\rho(k)$ is a derivation.[/guided]

[step:Prove that $\rho:\mathfrak k \to \operatorname{Der}(\mathfrak h)$ is a Lie algebra homomorphism]Let $k_1,k_2 \in \mathfrak k$ and $h \in \mathfrak h$. Since $s$ is a Lie algebra homomorphism, \begin{align*} s([k_1,k_2]_{\mathfrak k})=[s(k_1),s(k_2)]_{\mathfrak g}. \end{align*} Therefore \begin{align*} \iota(\rho([k_1,k_2]_{\mathfrak k})(h)) &= [s([k_1,k_2]_{\mathfrak k}),\iota(h)]_{\mathfrak g} \\ &= [[s(k_1),s(k_2)]_{\mathfrak g},\iota(h)]_{\mathfrak g}. \end{align*} By the Jacobi identity in $\mathfrak g$, \begin{align*} [[s(k_1),s(k_2)]_{\mathfrak g},\iota(h)]_{\mathfrak g} &= [s(k_1),[s(k_2),\iota(h)]_{\mathfrak g}]_{\mathfrak g} - [s(k_2),[s(k_1),\iota(h)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} Using the definition of $\rho$ twice, we get \begin{align*} \iota(\rho([k_1,k_2]_{\mathfrak k})(h)) &= [s(k_1),\iota(\rho(k_2)(h))]_{\mathfrak g} - [s(k_2),\iota(\rho(k_1)(h))]_{\mathfrak g} \\ &= \iota(\rho(k_1)(\rho(k_2)(h))) - \iota(\rho(k_2)(\rho(k_1)(h))) \\ &= \iota\bigl((\rho(k_1)\circ \rho(k_2)-\rho(k_2)\circ \rho(k_1))(h)\bigr). \end{align*} Since $\iota$ is injective, \begin{align*} \rho([k_1,k_2]_{\mathfrak k})(h) = (\rho(k_1)\circ \rho(k_2)-\rho(k_2)\circ \rho(k_1))(h). \end{align*} Thus \begin{align*} \rho([k_1,k_2]_{\mathfrak k}) = [\rho(k_1),\rho(k_2)]_{\operatorname{Der}(\mathfrak h)}. \end{align*} Together with linearity, this proves that $\rho:\mathfrak k \to \operatorname{Der}(\mathfrak h)$ is a Lie algebra homomorphism.[/step]

[guided]The Lie bracket on $\operatorname{Der}(\mathfrak h)$ is the commutator bracket: \begin{align*} [D_1,D_2]_{\operatorname{Der}(\mathfrak h)} = D_1\circ D_2-D_2\circ D_1. \end{align*} So to prove that $\rho$ is a Lie algebra homomorphism, we must prove \begin{align*} \rho([k_1,k_2]_{\mathfrak k}) = \rho(k_1)\circ \rho(k_2)-\rho(k_2)\circ \rho(k_1) \end{align*} for all $k_1,k_2 \in \mathfrak k$. Fix $k_1,k_2 \in \mathfrak k$ and $h \in \mathfrak h$. Because $s$ is a Lie algebra homomorphism, \begin{align*} s([k_1,k_2]_{\mathfrak k})=[s(k_1),s(k_2)]_{\mathfrak g}. \end{align*} Using the definition of $\rho$ on the left-hand side gives \begin{align*} \iota(\rho([k_1,k_2]_{\mathfrak k})(h)) &= [s([k_1,k_2]_{\mathfrak k}),\iota(h)]_{\mathfrak g} \\ &= [[s(k_1),s(k_2)]_{\mathfrak g},\iota(h)]_{\mathfrak g}. \end{align*} Now the Jacobi identity converts the bracket with $[s(k_1),s(k_2)]_{\mathfrak g}$ into the commutator of the two bracket operations. In $\mathfrak g$, \begin{align*} [[s(k_1),s(k_2)]_{\mathfrak g},\iota(h)]_{\mathfrak g} &= [s(k_1),[s(k_2),\iota(h)]_{\mathfrak g}]_{\mathfrak g} - [s(k_2),[s(k_1),\iota(h)]_{\mathfrak g}]_{\mathfrak g}. \end{align*} The two inner brackets are exactly the definition of $\rho$: \begin{align*} [s(k_i),\iota(h)]_{\mathfrak g}=\iota(\rho(k_i)(h)) \end{align*} for $i \in \{1,2\}$. Applying the definition again to the outer brackets gives \begin{align*} \iota(\rho([k_1,k_2]_{\mathfrak k})(h)) &= [s(k_1),\iota(\rho(k_2)(h))]_{\mathfrak g} - [s(k_2),\iota(\rho(k_1)(h))]_{\mathfrak g} \\ &= \iota(\rho(k_1)(\rho(k_2)(h))) - \iota(\rho(k_2)(\rho(k_1)(h))) \\ &= \iota\bigl((\rho(k_1)\circ \rho(k_2)-\rho(k_2)\circ \rho(k_1))(h)\bigr). \end{align*} Since $\iota$ is injective, we conclude \begin{align*} \rho([k_1,k_2]_{\mathfrak k})(h) = (\rho(k_1)\circ \rho(k_2)-\rho(k_2)\circ \rho(k_1))(h). \end{align*} Because $h \in \mathfrak h$ was arbitrary, \begin{align*} \rho([k_1,k_2]_{\mathfrak k}) = [\rho(k_1),\rho(k_2)]_{\operatorname{Der}(\mathfrak h)}. \end{align*} Together with the previously established linearity of $\rho$, this proves that $\rho$ is a Lie algebra homomorphism.[/guided]

[step:Check that the decomposition map preserves the semidirect product bracket]Equip the vector space $\mathfrak h \oplus \mathfrak k$ with the semidirect product Lie bracket determined by $\rho$: \begin{align*} [(h_1,k_1),(h_2,k_2)]_{\mathfrak h \rtimes_{\rho}\mathfrak k} := \bigl( [h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1), [k_1,k_2]_{\mathfrak k} \bigr). \end{align*} This Lie algebra is denoted $\mathfrak h \rtimes_{\rho} \mathfrak k$. Let $(h_1,k_1),(h_2,k_2) \in \mathfrak h \rtimes_{\rho} \mathfrak k$. Then, using bilinearity and skew-symmetry of the bracket in $\mathfrak g$, \begin{align*} [\Phi(h_1,k_1),\Phi(h_2,k_2)]_{\mathfrak g} &= [\iota(h_1)+s(k_1),\iota(h_2)+s(k_2)]_{\mathfrak g} \\ &= [\iota(h_1),\iota(h_2)]_{\mathfrak g} + [s(k_1),\iota(h_2)]_{\mathfrak g} + [\iota(h_1),s(k_2)]_{\mathfrak g} + [s(k_1),s(k_2)]_{\mathfrak g}. \end{align*} Each term is identified as follows: \begin{align*} [\iota(h_1),\iota(h_2)]_{\mathfrak g} &= \iota([h_1,h_2]_{\mathfrak h}), \\ [s(k_1),\iota(h_2)]_{\mathfrak g} &= \iota(\rho(k_1)(h_2)), \\ [\iota(h_1),s(k_2)]_{\mathfrak g} &= -[s(k_2),\iota(h_1)]_{\mathfrak g} = -\iota(\rho(k_2)(h_1)), \\ [s(k_1),s(k_2)]_{\mathfrak g} &= s([k_1,k_2]_{\mathfrak k}). \end{align*} Therefore \begin{align*} [\Phi(h_1,k_1),\Phi(h_2,k_2)]_{\mathfrak g} &= \iota\bigl([h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1)\bigr) +s([k_1,k_2]_{\mathfrak k}) \\ &= \Phi\bigl( [h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1), [k_1,k_2]_{\mathfrak k} \bigr) \\ &= \Phi([(h_1,k_1),(h_2,k_2)]_{\mathfrak h \rtimes_{\rho}\mathfrak k}). \end{align*} Thus $\Phi$ is a Lie algebra homomorphism. Since $\Phi$ was already proved to be a vector space isomorphism, it is an isomorphism of Lie algebras \begin{align*} \Phi:\mathfrak h \rtimes_{\rho}\mathfrak k \to \mathfrak g. \end{align*} This proves that the split extension identifies $\mathfrak g$ with the semidirect product $\mathfrak h \rtimes_{\rho}\mathfrak k$.[/step]

[guided]We have already proved that \begin{align*} \Phi:\mathfrak h \oplus \mathfrak k &\to \mathfrak g \\ (h,k) &\mapsto \iota(h)+s(k) \end{align*} is a vector space isomorphism. To upgrade this to a Lie algebra isomorphism, we must put the correct bracket on $\mathfrak h \oplus \mathfrak k$ and verify that $\Phi$ preserves brackets. Equip the vector space $\mathfrak h \oplus \mathfrak k$ with the semidirect product Lie bracket determined by the Lie algebra homomorphism $\rho:\mathfrak k \to \operatorname{Der}(\mathfrak h)$: \begin{align*} [(h_1,k_1),(h_2,k_2)]_{\mathfrak h \rtimes_{\rho}\mathfrak k} := \bigl( [h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1), [k_1,k_2]_{\mathfrak k} \bigr). \end{align*} This Lie algebra is denoted $\mathfrak h \rtimes_{\rho} \mathfrak k$. Let $(h_1,k_1),(h_2,k_2) \in \mathfrak h \rtimes_{\rho} \mathfrak k$. We compute the bracket of their images under $\Phi$. Bilinearity of the bracket in $\mathfrak g$ expands the bracket into four terms, and skew-symmetry accounts for the sign in the mixed term: \begin{align*} [\Phi(h_1,k_1),\Phi(h_2,k_2)]_{\mathfrak g} &= [\iota(h_1)+s(k_1),\iota(h_2)+s(k_2)]_{\mathfrak g} \\ &= [\iota(h_1),\iota(h_2)]_{\mathfrak g} + [s(k_1),\iota(h_2)]_{\mathfrak g} + [\iota(h_1),s(k_2)]_{\mathfrak g} + [s(k_1),s(k_2)]_{\mathfrak g}. \end{align*} Each of these four terms has already been identified by the construction. Since $\iota$ and $s$ are Lie algebra homomorphisms, and since $\rho$ was defined by $\iota(\rho(k)(h))=[s(k),\iota(h)]_{\mathfrak g}$, we have \begin{align*} [\iota(h_1),\iota(h_2)]_{\mathfrak g} &= \iota([h_1,h_2]_{\mathfrak h}), \\ [s(k_1),\iota(h_2)]_{\mathfrak g} &= \iota(\rho(k_1)(h_2)), \\ [\iota(h_1),s(k_2)]_{\mathfrak g} &= -[s(k_2),\iota(h_1)]_{\mathfrak g} = -\iota(\rho(k_2)(h_1)), \\ [s(k_1),s(k_2)]_{\mathfrak g} &= s([k_1,k_2]_{\mathfrak k}). \end{align*} Substituting these identities into the expanded bracket gives \begin{align*} [\Phi(h_1,k_1),\Phi(h_2,k_2)]_{\mathfrak g} &= \iota\bigl([h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1)\bigr) +s([k_1,k_2]_{\mathfrak k}) \\ &= \Phi\bigl( [h_1,h_2]_{\mathfrak h} +\rho(k_1)(h_2) -\rho(k_2)(h_1), [k_1,k_2]_{\mathfrak k} \bigr) \\ &= \Phi([(h_1,k_1),(h_2,k_2)]_{\mathfrak h \rtimes_{\rho}\mathfrak k}). \end{align*} Thus $\Phi$ preserves the Lie bracket. Since $\Phi$ is already a vector space isomorphism, it is an isomorphism of Lie algebras \begin{align*} \Phi:\mathfrak h \rtimes_{\rho}\mathfrak k \to \mathfrak g. \end{align*} Therefore the split short exact sequence identifies $\mathfrak g$ with the semidirect product $\mathfrak h \rtimes_{\rho}\mathfrak k$.[/guided]