[proofplan] We compare the derived sequence of $\mathfrak g$ with the derived sequence of its image $\varphi(\mathfrak g)$. The homomorphism identity $\varphi([x,y]_{\mathfrak g}) = [\varphi(x),\varphi(y)]_{\mathfrak h}$ shows that taking brackets commutes with applying $\varphi$, provided we restrict the codomain to the image. An induction proves that each derived term of the image is exactly the image of the corresponding derived term of $\mathfrak g$. Since solvability means that one derived term of $\mathfrak g$ is zero, the corresponding derived term of $\varphi(\mathfrak g)$ is also zero. [/proofplan] [step:Declare the two derived sequences and the image Lie algebra] Let $\mathfrak a := \varphi(\mathfrak g) \subset \mathfrak h$ denote the image of $\varphi$. Since $\varphi$ is linear, $\mathfrak a$ is a $k$-linear subspace of $\mathfrak h$. If $u,v \in \mathfrak a$, then there exist $x,y \in \mathfrak g$ such that $u = \varphi(x)$ and $v = \varphi(y)$; using that $\varphi$ is a Lie algebra homomorphism, \begin{align*} [u,v]_{\mathfrak h} = [\varphi(x),\varphi(y)]_{\mathfrak h} = \varphi([x,y]_{\mathfrak g}) \in \mathfrak a. \end{align*} Thus $\mathfrak a$ is a Lie subalgebra of $\mathfrak h$. Define the derived sequence $(\mathfrak g_i)_{i \geq 0}$ of $\mathfrak g$ by \begin{align*} \mathfrak g_0 &:= \mathfrak g, & \mathfrak g_{i+1} &:= [\mathfrak g_i,\mathfrak g_i]_{\mathfrak g} \quad\text{for every } i \geq 0. \end{align*} Here $[\mathfrak g_i,\mathfrak g_i]_{\mathfrak g}$ denotes the $k$-linear span of all brackets $[x,y]_{\mathfrak g}$ with $x,y \in \mathfrak g_i$. Define the derived sequence $(\mathfrak a_i)_{i \geq 0}$ of $\mathfrak a$ by \begin{align*} \mathfrak a_0 &:= \mathfrak a, & \mathfrak a_{i+1} &:= [\mathfrak a_i,\mathfrak a_i]_{\mathfrak h} \quad\text{for every } i \geq 0. \end{align*} Since the bracket on $\mathfrak a$ is the restriction of the bracket on $\mathfrak h$, this is exactly the derived sequence of the Lie algebra $\mathfrak a$. [/step] [step:Prove by induction that each derived image equals the corresponding image] We prove that \begin{align*} \mathfrak a_i = \varphi(\mathfrak g_i) \end{align*} for every integer $i \geq 0$. For $i = 0$, \begin{align*} \mathfrak a_0 = \mathfrak a = \varphi(\mathfrak g) = \varphi(\mathfrak g_0), \end{align*} so the assertion holds. Assume now that $i \geq 0$ and that $\mathfrak a_i = \varphi(\mathfrak g_i)$. We prove both inclusions for the next term. First let $w \in \varphi(\mathfrak g_{i+1})$. Then there exists $z \in \mathfrak g_{i+1}$ such that $w=\varphi(z)$. Since $\mathfrak g_{i+1} = [\mathfrak g_i,\mathfrak g_i]_{\mathfrak g}$, there exist an integer $N \geq 1$, scalars $c_1,\dots,c_N \in k$, and elements $x_1,\dots,x_N,y_1,\dots,y_N \in \mathfrak g_i$ such that \begin{align*} z = \sum_{r=1}^{N} c_r [x_r,y_r]_{\mathfrak g}. \end{align*} Using linearity of $\varphi$ and the homomorphism identity, \begin{align*} w &= \varphi(z) \\ &= \sum_{r=1}^{N} c_r \varphi([x_r,y_r]_{\mathfrak g}) \\ &= \sum_{r=1}^{N} c_r [\varphi(x_r),\varphi(y_r)]_{\mathfrak h}. \end{align*} For each $r$, the induction hypothesis gives $\varphi(x_r),\varphi(y_r) \in \varphi(\mathfrak g_i)=\mathfrak a_i$. Therefore $w \in [\mathfrak a_i,\mathfrak a_i]_{\mathfrak h}=\mathfrak a_{i+1}$. Conversely, let $w \in \mathfrak a_{i+1}$. Since $\mathfrak a_{i+1}=[\mathfrak a_i,\mathfrak a_i]_{\mathfrak h}$, there exist an integer $M \geq 1$, scalars $d_1,\dots,d_M \in k$, and elements $u_1,\dots,u_M,v_1,\dots,v_M \in \mathfrak a_i$ such that \begin{align*} w = \sum_{s=1}^{M} d_s [u_s,v_s]_{\mathfrak h}. \end{align*} By the induction hypothesis, $\mathfrak a_i=\varphi(\mathfrak g_i)$. Hence for each $s$ there exist $p_s,q_s \in \mathfrak g_i$ such that \begin{align*} u_s=\varphi(p_s), \qquad v_s=\varphi(q_s). \end{align*} Thus \begin{align*} w &= \sum_{s=1}^{M} d_s [\varphi(p_s),\varphi(q_s)]_{\mathfrak h} \\ &= \sum_{s=1}^{M} d_s \varphi([p_s,q_s]_{\mathfrak g}) \\ &= \varphi\left(\sum_{s=1}^{M} d_s [p_s,q_s]_{\mathfrak g}\right). \end{align*} The element $\sum_{s=1}^{M} d_s [p_s,q_s]_{\mathfrak g}$ lies in $[\mathfrak g_i,\mathfrak g_i]_{\mathfrak g}=\mathfrak g_{i+1}$, so $w \in \varphi(\mathfrak g_{i+1})$. Therefore $\mathfrak a_{i+1}=\varphi(\mathfrak g_{i+1})$. By induction, $\mathfrak a_i=\varphi(\mathfrak g_i)$ for every $i \geq 0$. [guided] The goal is to show that the operation “take the next derived algebra” is compatible with passing through the homomorphism $\varphi$. We prove the exact formula \begin{align*} \mathfrak a_i = \varphi(\mathfrak g_i) \end{align*} for every $i \geq 0$. The base case is the definition of the image: \begin{align*} \mathfrak a_0 = \mathfrak a = \varphi(\mathfrak g) = \varphi(\mathfrak g_0). \end{align*} Now assume that $\mathfrak a_i=\varphi(\mathfrak g_i)$ for some fixed integer $i \geq 0$. We need to prove \begin{align*} \mathfrak a_{i+1}=\varphi(\mathfrak g_{i+1}). \end{align*} This requires two inclusions. For the inclusion $\varphi(\mathfrak g_{i+1}) \subset \mathfrak a_{i+1}$, take $w \in \varphi(\mathfrak g_{i+1})$. Then $w=\varphi(z)$ for some $z \in \mathfrak g_{i+1}$. By definition, $\mathfrak g_{i+1}$ is the $k$-linear span of brackets of elements of $\mathfrak g_i$, so there are an integer $N \geq 1$, scalars $c_1,\dots,c_N \in k$, and elements $x_1,\dots,x_N,y_1,\dots,y_N \in \mathfrak g_i$ with \begin{align*} z = \sum_{r=1}^{N} c_r [x_r,y_r]_{\mathfrak g}. \end{align*} Applying $\varphi$, using its linearity, and then using the homomorphism identity gives \begin{align*} w &= \varphi(z) \\ &= \sum_{r=1}^{N} c_r \varphi([x_r,y_r]_{\mathfrak g}) \\ &= \sum_{r=1}^{N} c_r [\varphi(x_r),\varphi(y_r)]_{\mathfrak h}. \end{align*} Because $x_r,y_r \in \mathfrak g_i$, the induction hypothesis gives $\varphi(x_r),\varphi(y_r) \in \varphi(\mathfrak g_i)=\mathfrak a_i$. Hence the last expression is a $k$-linear combination of brackets of elements of $\mathfrak a_i$, which means \begin{align*} w \in [\mathfrak a_i,\mathfrak a_i]_{\mathfrak h}=\mathfrak a_{i+1}. \end{align*} For the reverse inclusion $\mathfrak a_{i+1} \subset \varphi(\mathfrak g_{i+1})$, take $w \in \mathfrak a_{i+1}$. Since $\mathfrak a_{i+1}$ is the $k$-linear span of brackets of elements of $\mathfrak a_i$, there are an integer $M \geq 1$, scalars $d_1,\dots,d_M \in k$, and elements $u_1,\dots,u_M,v_1,\dots,v_M \in \mathfrak a_i$ such that \begin{align*} w = \sum_{s=1}^{M} d_s [u_s,v_s]_{\mathfrak h}. \end{align*} The induction hypothesis says $\mathfrak a_i=\varphi(\mathfrak g_i)$, so each $u_s$ and $v_s$ has a preimage inside $\mathfrak g_i$. Thus, for every $s$, choose $p_s,q_s \in \mathfrak g_i$ such that \begin{align*} u_s=\varphi(p_s), \qquad v_s=\varphi(q_s). \end{align*} Substituting these preimages and using the homomorphism identity, \begin{align*} w &= \sum_{s=1}^{M} d_s [\varphi(p_s),\varphi(q_s)]_{\mathfrak h} \\ &= \sum_{s=1}^{M} d_s \varphi([p_s,q_s]_{\mathfrak g}) \\ &= \varphi\left(\sum_{s=1}^{M} d_s [p_s,q_s]_{\mathfrak g}\right). \end{align*} The element inside $\varphi$ belongs to $[\mathfrak g_i,\mathfrak g_i]_{\mathfrak g}=\mathfrak g_{i+1}$. Therefore $w \in \varphi(\mathfrak g_{i+1})$. Both inclusions hold, so $\mathfrak a_{i+1}=\varphi(\mathfrak g_{i+1})$. The induction is complete. [/guided] [/step] [step:Use termination of the derived sequence of $\mathfrak g$ to terminate the image sequence] Since $\mathfrak g$ is solvable, there exists an integer $m \geq 0$ such that \begin{align*} \mathfrak g_m = \{0\}. \end{align*} Using the identity proved above at index $m$, \begin{align*} \mathfrak a_m = \varphi(\mathfrak g_m) = \varphi(\{0\}) = \{0\}. \end{align*} Thus the derived sequence of $\mathfrak a=\varphi(\mathfrak g)$ terminates at zero. Therefore $\varphi(\mathfrak g)$ is solvable. [/step]