[proofplan]
We verify the Lie algebra axioms directly from the defining bracket. Bilinearity follows by expanding the formula, using bilinearity in $\mathfrak h$ and $\mathfrak k$, and using the $F$-linearity of the action map $\rho:\mathfrak k\to\operatorname{Der}_F(\mathfrak h)$. Alternation is checked directly by evaluating $[(h,k),(h,k)]_{\rtimes}$, which also gives skew-symmetry by bilinearity. The Jacobi identity is checked componentwise: the $\mathfrak k$-component is the Jacobi identity in $\mathfrak k$, while the $\mathfrak h$-component splits into the Jacobi identity in $\mathfrak h$, the derivation rule for each $\rho(k)$, and the homomorphism identity $\rho([k_i,k_j]_{\mathfrak k})=[\rho(k_i),\rho(k_j)]$. Finally, the two canonical embeddings are inspected directly from the bracket formula.
[/proofplan]
[step:Verify bilinearity and alternation of the bracket]
Let $x_1=(h_1,k_1)$ and $x_2=(h_2,k_2)$ be elements of $\mathfrak h \oplus \mathfrak k$. Since $[\cdot,\cdot]_{\mathfrak h}$ and $[\cdot,\cdot]_{\mathfrak k}$ are $F$-bilinear, each $\rho(k):\mathfrak h \to \mathfrak h$ is $F$-linear, and $\rho:\mathfrak k\to\operatorname{Der}_F(\mathfrak h)$ is $F$-linear, the formula defining $[\cdot,\cdot]_{\rtimes}$ is $F$-bilinear in $x_1$ and $x_2$.
For alternation, let $x=(h,k) \in \mathfrak h \oplus \mathfrak k$. Since $\mathfrak h$ and $\mathfrak k$ are Lie algebras, their brackets are alternating, so $[h,h]_{\mathfrak h}=0$ and $[k,k]_{\mathfrak k}=0$. Therefore
\begin{align*}
[x,x]_{\rtimes}
&=
[(h,k),(h,k)]_{\rtimes} \\
&=
\bigl([h,h]_{\mathfrak h}+\rho(k)(h)-\rho(k)(h),[k,k]_{\mathfrak k}\bigr) \\
&=
(0,0).
\end{align*}
Thus $[\cdot,\cdot]_{\rtimes}$ is alternating. Since the bracket is bilinear, alternation also implies skew-symmetry: applying alternation to $x_1+x_2$ gives
\begin{align*}
0
&=[x_1+x_2,x_1+x_2]_{\rtimes} \\
&=[x_1,x_2]_{\rtimes}+[x_2,x_1]_{\rtimes},
\end{align*}
and hence $[x_2,x_1]_{\rtimes}=-[x_1,x_2]_{\rtimes}$.
[/step]
[step:Expand the Jacobi expression componentwise]
Let $x_i=(h_i,k_i) \in \mathfrak h \oplus \mathfrak k$ for $i \in \{1,2,3\}$. Define $D_i := \rho(k_i) \in \operatorname{Der}_F(\mathfrak h)$ for each $i$. Since $\rho$ is a Lie algebra homomorphism,
\begin{align*}
[D_i,D_j] = D_iD_j-D_jD_i = \rho([k_i,k_j]_{\mathfrak k})
\end{align*}
for all $i,j \in \{1,2,3\}$. Since $D_i$ is a derivation of $\mathfrak h$,
\begin{align*}
D_i([a,b]_{\mathfrak h})=[D_i(a),b]_{\mathfrak h}+[a,D_i(b)]_{\mathfrak h}
\end{align*}
for all $a,b \in \mathfrak h$.
Set
\begin{align*}
J(x_1,x_2,x_3)
:=
[x_1,[x_2,x_3]_{\rtimes}]_{\rtimes}
+[x_2,[x_3,x_1]_{\rtimes}]_{\rtimes}
+[x_3,[x_1,x_2]_{\rtimes}]_{\rtimes}.
\end{align*}
The $\mathfrak k$-component of $J(x_1,x_2,x_3)$ is
\begin{align*}
[k_1,[k_2,k_3]_{\mathfrak k}]_{\mathfrak k}
+[k_2,[k_3,k_1]_{\mathfrak k}]_{\mathfrak k}
+[k_3,[k_1,k_2]_{\mathfrak k}]_{\mathfrak k},
\end{align*}
which is $0$ by the Jacobi identity in $\mathfrak k$.
[guided]
We check the Jacobi identity for three arbitrary elements
$x_i=(h_i,k_i) \in \mathfrak h \oplus \mathfrak k$, where $i \in \{1,2,3\}$. The bracket has two components, so the Jacobi expression can vanish only if both its $\mathfrak h$-component and its $\mathfrak k$-component vanish.
Define $D_i := \rho(k_i) \in \operatorname{Der}_F(\mathfrak h)$ for each $i$. This notation records the action of the $\mathfrak k$-part of $x_i$ on $\mathfrak h$. Because $\rho$ is a Lie algebra homomorphism, the commutator of the two derivations $D_i$ and $D_j$ is the derivation attached to the bracket $[k_i,k_j]_{\mathfrak k}$:
\begin{align*}
[D_i,D_j]=D_iD_j-D_jD_i=\rho([k_i,k_j]_{\mathfrak k}).
\end{align*}
Because $D_i$ is a derivation of the Lie algebra $\mathfrak h$, it satisfies
\begin{align*}
D_i([a,b]_{\mathfrak h})=[D_i(a),b]_{\mathfrak h}+[a,D_i(b)]_{\mathfrak h}
\end{align*}
for all $a,b \in \mathfrak h$.
Now define the Jacobi expression
\begin{align*}
J(x_1,x_2,x_3)
:=
[x_1,[x_2,x_3]_{\rtimes}]_{\rtimes}
+[x_2,[x_3,x_1]_{\rtimes}]_{\rtimes}
+[x_3,[x_1,x_2]_{\rtimes}]_{\rtimes}.
\end{align*}
The second component of $[x_i,x_j]_{\rtimes}$ is exactly $[k_i,k_j]_{\mathfrak k}$. Therefore the $\mathfrak k$-component of $J(x_1,x_2,x_3)$ is
\begin{align*}
[k_1,[k_2,k_3]_{\mathfrak k}]_{\mathfrak k}
+[k_2,[k_3,k_1]_{\mathfrak k}]_{\mathfrak k}
+[k_3,[k_1,k_2]_{\mathfrak k}]_{\mathfrak k}.
\end{align*}
This is $0$ by the Jacobi identity in the Lie algebra $\mathfrak k$. Thus only the $\mathfrak h$-component remains to be checked.
[/guided]
[/step]
[step:Cancel the $\mathfrak h$ component of the Jacobi expression]
The $\mathfrak h$-component of $[x_1,[x_2,x_3]_{\rtimes}]_{\rtimes}$ equals
\begin{align*}
&[h_1,[h_2,h_3]_{\mathfrak h}+D_2(h_3)-D_3(h_2)]_{\mathfrak h}
+D_1([h_2,h_3]_{\mathfrak h}+D_2(h_3)-D_3(h_2)) \\
&\qquad
-\rho([k_2,k_3]_{\mathfrak k})(h_1).
\end{align*}
Using $\rho([k_2,k_3]_{\mathfrak k})=[D_2,D_3]$ and expanding by bilinearity and the derivation rule gives
\begin{align*}
&[h_1,[h_2,h_3]_{\mathfrak h}]_{\mathfrak h}
+[h_1,D_2(h_3)]_{\mathfrak h}
-[h_1,D_3(h_2)]_{\mathfrak h} \\
&\quad
+[D_1(h_2),h_3]_{\mathfrak h}
+[h_2,D_1(h_3)]_{\mathfrak h}
+D_1D_2(h_3)-D_1D_3(h_2)-D_2D_3(h_1)+D_3D_2(h_1).
\end{align*}
Adding the two cyclic analogues, the terms
\begin{align*}
[h_1,[h_2,h_3]_{\mathfrak h}]_{\mathfrak h}
+[h_2,[h_3,h_1]_{\mathfrak h}]_{\mathfrak h}
+[h_3,[h_1,h_2]_{\mathfrak h}]_{\mathfrak h}
\end{align*}
cancel by the Jacobi identity in $\mathfrak h$. The terms involving one bracket in $\mathfrak h$ and one derivation are
\begin{align*}
&[h_1,D_2(h_3)]_{\mathfrak h}-[h_1,D_3(h_2)]_{\mathfrak h}+[D_1(h_2),h_3]_{\mathfrak h}+[h_2,D_1(h_3)]_{\mathfrak h} \\
&\quad
+[h_2,D_3(h_1)]_{\mathfrak h}-[h_2,D_1(h_3)]_{\mathfrak h}+[D_2(h_3),h_1]_{\mathfrak h}+[h_3,D_2(h_1)]_{\mathfrak h} \\
&\quad
+[h_3,D_1(h_2)]_{\mathfrak h}-[h_3,D_2(h_1)]_{\mathfrak h}+[D_3(h_1),h_2]_{\mathfrak h}+[h_1,D_3(h_2)]_{\mathfrak h}.
\end{align*}
They cancel pairwise: the pairs $[h_1,D_2(h_3)]_{\mathfrak h}+[D_2(h_3),h_1]_{\mathfrak h}$, $[D_1(h_2),h_3]_{\mathfrak h}+[h_3,D_1(h_2)]_{\mathfrak h}$, and $[h_2,D_3(h_1)]_{\mathfrak h}+[D_3(h_1),h_2]_{\mathfrak h}$ vanish by skew-symmetry in $\mathfrak h$, while the remaining three pairs cancel as identical terms with opposite signs. The second-order derivation terms are
\begin{align*}
&D_1D_2(h_3)-D_1D_3(h_2)-D_2D_3(h_1)+D_3D_2(h_1) \\
&\quad
+D_2D_3(h_1)-D_2D_1(h_3)-D_3D_1(h_2)+D_1D_3(h_2) \\
&\quad
+D_3D_1(h_2)-D_3D_2(h_1)-D_1D_2(h_3)+D_2D_1(h_3),
\end{align*}
which cancel term by term. Hence the $\mathfrak h$-component of $J(x_1,x_2,x_3)$ is $0$.
[guided]
We now prove that the $\mathfrak h$-component of the Jacobi expression also vanishes. First compute the first cyclic term. Since
\begin{align*}
[x_2,x_3]_{\rtimes}
=
\bigl([h_2,h_3]_{\mathfrak h}+D_2(h_3)-D_3(h_2),[k_2,k_3]_{\mathfrak k}\bigr),
\end{align*}
the definition of the semidirect bracket gives the $\mathfrak h$-component of $[x_1,[x_2,x_3]_{\rtimes}]_{\rtimes}$ as
\begin{align*}
&[h_1,[h_2,h_3]_{\mathfrak h}+D_2(h_3)-D_3(h_2)]_{\mathfrak h}
+D_1([h_2,h_3]_{\mathfrak h}+D_2(h_3)-D_3(h_2)) \\
&\qquad
-\rho([k_2,k_3]_{\mathfrak k})(h_1).
\end{align*}
The last term is where the homomorphism property of $\rho$ is used. Since $\rho([k_2,k_3]_{\mathfrak k})=[D_2,D_3]=D_2D_3-D_3D_2$, this expression becomes
\begin{align*}
&[h_1,[h_2,h_3]_{\mathfrak h}]_{\mathfrak h}
+[h_1,D_2(h_3)]_{\mathfrak h}
-[h_1,D_3(h_2)]_{\mathfrak h} \\
&\quad
+D_1([h_2,h_3]_{\mathfrak h})
+D_1D_2(h_3)-D_1D_3(h_2)
-D_2D_3(h_1)+D_3D_2(h_1).
\end{align*}
Now use that $D_1$ is a derivation of $\mathfrak h$:
\begin{align*}
D_1([h_2,h_3]_{\mathfrak h})
=
[D_1(h_2),h_3]_{\mathfrak h}
+[h_2,D_1(h_3)]_{\mathfrak h}.
\end{align*}
Thus the first cyclic term contributes
\begin{align*}
&[h_1,[h_2,h_3]_{\mathfrak h}]_{\mathfrak h}
+[h_1,D_2(h_3)]_{\mathfrak h}
-[h_1,D_3(h_2)]_{\mathfrak h} \\
&\quad
+[D_1(h_2),h_3]_{\mathfrak h}
+[h_2,D_1(h_3)]_{\mathfrak h}
+D_1D_2(h_3)-D_1D_3(h_2)-D_2D_3(h_1)+D_3D_2(h_1).
\end{align*}
We add the two cyclic analogues obtained by replacing $(1,2,3)$ with $(2,3,1)$ and $(3,1,2)$. Three different kinds of terms appear.
First, the pure $\mathfrak h$-bracket terms are
\begin{align*}
[h_1,[h_2,h_3]_{\mathfrak h}]_{\mathfrak h}
+[h_2,[h_3,h_1]_{\mathfrak h}]_{\mathfrak h}
+[h_3,[h_1,h_2]_{\mathfrak h}]_{\mathfrak h},
\end{align*}
and these vanish by the Jacobi identity in $\mathfrak h$.
Second, the terms containing one derivation and one $\mathfrak h$-bracket are
\begin{align*}
&[h_1,D_2(h_3)]_{\mathfrak h}-[h_1,D_3(h_2)]_{\mathfrak h}+[D_1(h_2),h_3]_{\mathfrak h}+[h_2,D_1(h_3)]_{\mathfrak h} \\
&\quad
+[h_2,D_3(h_1)]_{\mathfrak h}-[h_2,D_1(h_3)]_{\mathfrak h}+[D_2(h_3),h_1]_{\mathfrak h}+[h_3,D_2(h_1)]_{\mathfrak h} \\
&\quad
+[h_3,D_1(h_2)]_{\mathfrak h}-[h_3,D_2(h_1)]_{\mathfrak h}+[D_3(h_1),h_2]_{\mathfrak h}+[h_1,D_3(h_2)]_{\mathfrak h}.
\end{align*}
Now pair them explicitly. The sums
\begin{align*}
[h_1,D_2(h_3)]_{\mathfrak h}+[D_2(h_3),h_1]_{\mathfrak h},\qquad
[D_1(h_2),h_3]_{\mathfrak h}+[h_3,D_1(h_2)]_{\mathfrak h},
\end{align*}
and
\begin{align*}
[h_2,D_3(h_1)]_{\mathfrak h}+[D_3(h_1),h_2]_{\mathfrak h}
\end{align*}
vanish by skew-symmetry of $[\cdot,\cdot]_{\mathfrak h}$. The remaining three cancellations are literal opposite-sign cancellations:
\begin{align*}
-[h_1,D_3(h_2)]_{\mathfrak h}+[h_1,D_3(h_2)]_{\mathfrak h}=0,
\end{align*}
\begin{align*}
[h_2,D_1(h_3)]_{\mathfrak h}-[h_2,D_1(h_3)]_{\mathfrak h}=0,
\end{align*}
and
\begin{align*}
[h_3,D_2(h_1)]_{\mathfrak h}-[h_3,D_2(h_1)]_{\mathfrak h}=0.
\end{align*}
Third, the second-order derivation terms are
\begin{align*}
&D_1D_2(h_3)-D_1D_3(h_2)-D_2D_3(h_1)+D_3D_2(h_1) \\
&\quad
+D_2D_3(h_1)-D_2D_1(h_3)-D_3D_1(h_2)+D_1D_3(h_2) \\
&\quad
+D_3D_1(h_2)-D_3D_2(h_1)-D_1D_2(h_3)+D_2D_1(h_3).
\end{align*}
Each displayed term appears once with coefficient $1$ and once with coefficient $-1$, so their sum is $0$. Therefore the $\mathfrak h$-component of $J(x_1,x_2,x_3)$ is $0$.
[/guided]
[/step]
[step:Conclude the Jacobi identity for the semidirect bracket]
The previous two steps show that both the $\mathfrak h$-component and the $\mathfrak k$-component of $J(x_1,x_2,x_3)$ vanish. Hence
\begin{align*}
[x_1,[x_2,x_3]_{\rtimes}]_{\rtimes}
+[x_2,[x_3,x_1]_{\rtimes}]_{\rtimes}
+[x_3,[x_1,x_2]_{\rtimes}]_{\rtimes}
=0
\end{align*}
for all $x_1,x_2,x_3 \in \mathfrak h \oplus \mathfrak k$. Together with bilinearity and alternation, this proves that $\mathfrak h \rtimes_\rho \mathfrak k$ is a Lie algebra over $F$.
[/step]
[step:Identify $\mathfrak h$ as an ideal and $\mathfrak k$ as a subalgebra]
Define
\begin{align*}
i_{\mathfrak h}: \mathfrak h &\to \mathfrak h \rtimes_\rho \mathfrak k,
&
h &\mapsto (h,0),
\\
i_{\mathfrak k}: \mathfrak k &\to \mathfrak h \rtimes_\rho \mathfrak k,
&
k &\mapsto (0,k).
\end{align*}
Both maps are injective $F$-linear maps.
For $h,h' \in \mathfrak h$,
\begin{align*}
[i_{\mathfrak h}(h),i_{\mathfrak h}(h')]_{\rtimes}
=
[(h,0),(h',0)]_{\rtimes}
=
([h,h']_{\mathfrak h},0)
=
i_{\mathfrak h}([h,h']_{\mathfrak h}),
\end{align*}
so $i_{\mathfrak h}(\mathfrak h)$ is a Lie subalgebra. For any $(a,k) \in \mathfrak h \rtimes_\rho \mathfrak k$ and any $h \in \mathfrak h$,
\begin{align*}
[(a,k),(h,0)]_{\rtimes}
=
([a,h]_{\mathfrak h}+\rho(k)(h),0)
\in i_{\mathfrak h}(\mathfrak h).
\end{align*}
Thus $i_{\mathfrak h}(\mathfrak h)$ is an ideal.
For $k,k' \in \mathfrak k$,
\begin{align*}
[i_{\mathfrak k}(k),i_{\mathfrak k}(k')]_{\rtimes}
=
[(0,k),(0,k')]_{\rtimes}
=
(0,[k,k']_{\mathfrak k})
=
i_{\mathfrak k}([k,k']_{\mathfrak k}).
\end{align*}
Therefore $i_{\mathfrak k}(\mathfrak k)$ is a Lie subalgebra of $\mathfrak h \rtimes_\rho \mathfrak k$. This proves all asserted properties of the semidirect product Lie algebra.
[/step]
