[proofplan]
We compare the derived series of $\mathfrak g$ with the derived series of the quotient $\mathfrak g/\mathfrak a$. Solvability of the quotient forces a sufficiently high derived algebra of $\mathfrak g$ to lie inside $\mathfrak a$. Once inside $\mathfrak a$, further commutators are controlled by the derived series of $\mathfrak a$, and solvability of $\mathfrak a$ then forces the derived series of $\mathfrak g$ to vanish.
[/proofplan]
[step:Define the derived series and the quotient projection]
For any Lie algebra $\mathfrak h$ over $k$, define its derived series $(\mathfrak h^{(r)})_{r \geq 0}$ by
\begin{align*}
\mathfrak h^{(0)} &= \mathfrak h, \\
\mathfrak h^{(r+1)} &= [\mathfrak h^{(r)}, \mathfrak h^{(r)}]
\end{align*}
for every integer $r \geq 0$, where $[\mathfrak h^{(r)}, \mathfrak h^{(r)}]$ denotes the $k$-linear span of all brackets $[x,y]$ with $x,y \in \mathfrak h^{(r)}$.
Let
\begin{align*}
\pi: \mathfrak g &\to \mathfrak g/\mathfrak a \\
x &\mapsto x+\mathfrak a
\end{align*}
be the quotient Lie algebra homomorphism. Since $\mathfrak g/\mathfrak a$ is solvable, there exists an integer $m \geq 0$ such that
\begin{align*}
(\mathfrak g/\mathfrak a)^{(m)} = 0.
\end{align*}
Since $\mathfrak a$ is solvable, there exists an integer $n \geq 0$ such that
\begin{align*}
\mathfrak a^{(n)} = 0.
\end{align*}
[/step]
[step:Show that the quotient projection carries derived series onto derived series]
[claim:Images of derived series under a surjective Lie homomorphism]
Let $\varphi: \mathfrak h \to \mathfrak q$ be a surjective homomorphism of Lie algebras over $k$. Then for every integer $r \geq 0$,
\begin{align*}
\varphi(\mathfrak h^{(r)}) = \mathfrak q^{(r)}.
\end{align*}
[/claim]
[proof]
We prove the assertion by induction on $r$.
For $r=0$, one has $\mathfrak h^{(0)}=\mathfrak h$ and $\mathfrak q^{(0)}=\mathfrak q$. Since $\varphi$ is surjective,
\begin{align*}
\varphi(\mathfrak h^{(0)})=\varphi(\mathfrak h)=\mathfrak q=\mathfrak q^{(0)}.
\end{align*}
Assume that for some integer $r \geq 0$,
\begin{align*}
\varphi(\mathfrak h^{(r)}) = \mathfrak q^{(r)}.
\end{align*}
Because $\varphi$ preserves Lie brackets, for all $x,y \in \mathfrak h^{(r)}$,
\begin{align*}
\varphi([x,y]) = [\varphi(x),\varphi(y)].
\end{align*}
Therefore
\begin{align*}
\varphi(\mathfrak h^{(r+1)})
&= \varphi([\mathfrak h^{(r)},\mathfrak h^{(r)}]) \\
&= [\varphi(\mathfrak h^{(r)}),\varphi(\mathfrak h^{(r)})] \\
&= [\mathfrak q^{(r)},\mathfrak q^{(r)}] \\
&= \mathfrak q^{(r+1)}.
\end{align*}
The induction is complete.
[/proof]
Applying the claim to the surjective Lie homomorphism $\pi: \mathfrak g \to \mathfrak g/\mathfrak a$ gives
\begin{align*}
\pi(\mathfrak g^{(m)}) = (\mathfrak g/\mathfrak a)^{(m)} = 0.
\end{align*}
Thus every element of $\mathfrak g^{(m)}$ lies in $\ker \pi$. Since $\ker \pi=\mathfrak a$, we obtain
\begin{align*}
\mathfrak g^{(m)} \subset \mathfrak a.
\end{align*}
[guided]
The purpose of this step is to turn solvability of the quotient into an inclusion inside the ideal $\mathfrak a$. The quotient map is
\begin{align*}
\pi: \mathfrak g &\to \mathfrak g/\mathfrak a \\
x &\mapsto x+\mathfrak a.
\end{align*}
It is a surjective Lie algebra homomorphism because the bracket on $\mathfrak g/\mathfrak a$ is defined by
\begin{align*}
[x+\mathfrak a,y+\mathfrak a] = [x,y]+\mathfrak a.
\end{align*}
We first verify the general fact needed here. If $\varphi: \mathfrak h \to \mathfrak q$ is a surjective Lie algebra homomorphism, then $\varphi(\mathfrak h^{(r)})=\mathfrak q^{(r)}$ for every $r \geq 0$. For $r=0$, this is exactly surjectivity:
\begin{align*}
\varphi(\mathfrak h^{(0)})=\varphi(\mathfrak h)=\mathfrak q=\mathfrak q^{(0)}.
\end{align*}
If $\varphi(\mathfrak h^{(r)})=\mathfrak q^{(r)}$, then preservation of brackets gives
\begin{align*}
\varphi(\mathfrak h^{(r+1)})
&= \varphi([\mathfrak h^{(r)},\mathfrak h^{(r)}]) \\
&= [\varphi(\mathfrak h^{(r)}),\varphi(\mathfrak h^{(r)})] \\
&= [\mathfrak q^{(r)},\mathfrak q^{(r)}] \\
&= \mathfrak q^{(r+1)}.
\end{align*}
Thus the equality holds for all $r$ by induction.
Now apply this to $\pi$. Since $(\mathfrak g/\mathfrak a)^{(m)}=0$, we get
\begin{align*}
\pi(\mathfrak g^{(m)}) = (\mathfrak g/\mathfrak a)^{(m)} = 0.
\end{align*}
This says that every element of $\mathfrak g^{(m)}$ maps to the zero coset. The kernel of the quotient map is exactly $\mathfrak a$, so
\begin{align*}
\mathfrak g^{(m)} \subset \mathfrak a.
\end{align*}
[/guided]
[/step]
[step:Compare the later derived terms of $\mathfrak g$ with those of $\mathfrak a$]
We prove by induction on $r \geq 0$ that
\begin{align*}
\mathfrak g^{(m+r)} \subset \mathfrak a^{(r)}.
\end{align*}
For $r=0$, this is precisely the inclusion already proved:
\begin{align*}
\mathfrak g^{(m)} \subset \mathfrak a = \mathfrak a^{(0)}.
\end{align*}
Assume that for some integer $r \geq 0$,
\begin{align*}
\mathfrak g^{(m+r)} \subset \mathfrak a^{(r)}.
\end{align*}
Taking brackets of both sides with themselves gives
\begin{align*}
\mathfrak g^{(m+r+1)}
&= [\mathfrak g^{(m+r)},\mathfrak g^{(m+r)}] \\
&\subset [\mathfrak a^{(r)},\mathfrak a^{(r)}] \\
&= \mathfrak a^{(r+1)}.
\end{align*}
Thus
\begin{align*}
\mathfrak g^{(m+r)} \subset \mathfrak a^{(r)}
\end{align*}
for every integer $r \geq 0$.
[/step]
[step:Conclude that the derived series of $\mathfrak g$ vanishes]
Taking $r=n$ in the inclusion from the previous step gives
\begin{align*}
\mathfrak g^{(m+n)} \subset \mathfrak a^{(n)}.
\end{align*}
By the choice of $n$, we have $\mathfrak a^{(n)}=0$, and therefore
\begin{align*}
\mathfrak g^{(m+n)} = 0.
\end{align*}
Hence the derived series of $\mathfrak g$ reaches zero after finitely many steps. Therefore $\mathfrak g$ is solvable.
[/step]
