[proofplan]
We prove both implications using the adjoint representation. If $\mathfrak g$ is solvable, [Lie's theorem](/theorems/3754) triangularizes the operators $\operatorname{ad}x$, and the operators coming from $[\mathfrak g,\mathfrak g]$ become strictly upper triangular, forcing the relevant traces to vanish. Conversely, the stated trace condition is exactly the Cartan trace criterion for the Lie algebra $\operatorname{ad}\mathfrak g \subseteq \mathfrak{gl}(\mathfrak g)$. Once $\operatorname{ad}\mathfrak g$ is solvable, the kernel of $\operatorname{ad}$ is the center $Z(\mathfrak g)$, so $\mathfrak g$ is an extension of a solvable Lie algebra by an abelian ideal and is therefore solvable.
[/proofplan]
[step:Triangularize the adjoint representation when $\mathfrak g$ is solvable]
Assume first that $\mathfrak g$ is solvable. Let $V := \mathfrak g$, regarded as a finite-dimensional $F$-[vector space](/page/Vector%20Space), and let
\begin{align*}
\rho: \mathfrak g &\to \mathfrak{gl}(V) \\
x &\mapsto \operatorname{ad}x
\end{align*}
be the adjoint representation.
Since $F$ is algebraically closed of characteristic $0$, $V$ is finite-dimensional, and $\mathfrak g$ is solvable, [Lie's theorem](/theorems/3802) applies to $\rho$ (citing a result not yet in the wiki: [Lie's Theorem](/theorems/3803)). Hence there exists a basis of $V$ in which every operator $\operatorname{ad}y$, with $y \in \mathfrak g$, is represented by an upper triangular matrix.
[guided]
Assume $\mathfrak g$ is solvable. We want to convert solvability into a concrete matrix statement about the operators appearing in the Killing form. Define $V := \mathfrak g$ as an $F$-vector space, and define the adjoint representation
\begin{align*}
\rho: \mathfrak g &\to \mathfrak{gl}(V) \\
x &\mapsto \operatorname{ad}x.
\end{align*}
This is a representation because the Jacobi identity gives
\begin{align*}
[\operatorname{ad}x,\operatorname{ad}y]=\operatorname{ad}[x,y]
\end{align*}
for all $x,y \in \mathfrak g$.
We apply Lie's theorem to this representation (citing a result not yet in the wiki: Lie's Theorem). Its hypotheses are satisfied: the field $F$ is algebraically closed, $\operatorname{char}F=0$, the vector space $V$ is finite-dimensional, and the Lie algebra $\mathfrak g$ is solvable by assumption. Therefore there is a basis of $V$ in which every $\operatorname{ad}y$, for $y \in \mathfrak g$, is represented by an upper triangular matrix. This basis is the one in which the trace computation becomes transparent.
[/guided]
[/step]
[step:Show that commutator adjoint operators have zero diagonal]
Let $x \in [\mathfrak g,\mathfrak g]$. Choose elements $a_1,b_1,\dots,a_m,b_m \in \mathfrak g$ and scalars $\lambda_1,\dots,\lambda_m \in F$ such that
\begin{align*}
x=\sum_{r=1}^{m}\lambda_r[a_r,b_r].
\end{align*}
In the triangularizing basis from the previous step, each $\operatorname{ad}a_r$ and $\operatorname{ad}b_r$ is upper triangular. Therefore each commutator
\begin{align*}
[\operatorname{ad}a_r,\operatorname{ad}b_r]
\end{align*}
is upper triangular with zero diagonal, because the diagonal entries of $AB$ and $BA$ agree for upper triangular matrices $A$ and $B$. Since
\begin{align*}
\operatorname{ad}x
= \sum_{r=1}^{m}\lambda_r \operatorname{ad}[a_r,b_r]
= \sum_{r=1}^{m}\lambda_r[\operatorname{ad}a_r,\operatorname{ad}b_r],
\end{align*}
the matrix of $\operatorname{ad}x$ is upper triangular with zero diagonal.
[guided]
Let $x \in [\mathfrak g,\mathfrak g]$. By the definition of the derived algebra, $x$ is a finite $F$-linear combination of brackets, so there exist $a_1,b_1,\dots,a_m,b_m \in \mathfrak g$ and $\lambda_1,\dots,\lambda_m \in F$ such that
\begin{align*}
x=\sum_{r=1}^{m}\lambda_r[a_r,b_r].
\end{align*}
In the basis supplied by Lie's theorem, every $\operatorname{ad}a_r$ and every $\operatorname{ad}b_r$ is upper triangular. If $A$ and $B$ are upper triangular matrices, then $AB$ and $BA$ are upper triangular, and their $i$th diagonal entries are both $A_{ii}B_{ii}$. Hence the commutator $AB-BA$ is upper triangular with zero diagonal.
Using the representation identity
\begin{align*}
[\operatorname{ad}a_r,\operatorname{ad}b_r]=\operatorname{ad}[a_r,b_r],
\end{align*}
we obtain
\begin{align*}
\operatorname{ad}x
= \sum_{r=1}^{m}\lambda_r \operatorname{ad}[a_r,b_r]
= \sum_{r=1}^{m}\lambda_r[\operatorname{ad}a_r,\operatorname{ad}b_r].
\end{align*}
A finite linear combination of upper triangular matrices with zero diagonal again has those two properties. Therefore $\operatorname{ad}x$ is upper triangular with zero diagonal.
[/guided]
[/step]
[step:Compute the trace pairing in the solvable case]
Let $x \in [\mathfrak g,\mathfrak g]$ and $y \in \mathfrak g$. In the triangularizing basis, $\operatorname{ad}x$ is upper triangular with zero diagonal and $\operatorname{ad}y$ is upper triangular. Their product $\operatorname{ad}x \circ \operatorname{ad}y$ is upper triangular with zero diagonal, so
\begin{align*}
\kappa(x,y)
= \operatorname{tr}_F(\operatorname{ad}x \circ \operatorname{ad}y)
=0.
\end{align*}
This proves the forward implication.
[/step]
[step:Apply the Cartan trace criterion to the adjoint image]
Conversely, assume that
\begin{align*}
\kappa(x,y)=0
\end{align*}
for every $x \in [\mathfrak g,\mathfrak g]$ and every $y \in \mathfrak g$. Define the adjoint image
\begin{align*}
\mathfrak h := \operatorname{ad}\mathfrak g \subseteq \mathfrak{gl}(\mathfrak g).
\end{align*}
The identity
\begin{align*}
[\operatorname{ad}x,\operatorname{ad}y]=\operatorname{ad}[x,y]
\end{align*}
implies
\begin{align*}
[\mathfrak h,\mathfrak h]=\operatorname{ad}[\mathfrak g,\mathfrak g].
\end{align*}
Thus, for every $A \in [\mathfrak h,\mathfrak h]$ and every $B \in \mathfrak h$, there exist $x \in [\mathfrak g,\mathfrak g]$ and $y \in \mathfrak g$ such that $A=\operatorname{ad}x$ and $B=\operatorname{ad}y$, and hence
\begin{align*}
\operatorname{tr}_F(A \circ B)
= \operatorname{tr}_F(\operatorname{ad}x \circ \operatorname{ad}y)
= \kappa(x,y)
=0.
\end{align*}
By the Cartan trace criterion for linear Lie algebras (citing a result not yet in the wiki: Cartan Trace Criterion), $\mathfrak h$ is solvable.
[guided]
Now assume the trace condition in the theorem statement:
\begin{align*}
\kappa(x,y)=0
\end{align*}
for all $x \in [\mathfrak g,\mathfrak g]$ and all $y \in \mathfrak g$.
We pass from $\mathfrak g$ to its adjoint image because the trace condition is naturally a condition on endomorphisms. Define
\begin{align*}
\mathfrak h := \operatorname{ad}\mathfrak g \subseteq \mathfrak{gl}(\mathfrak g).
\end{align*}
This is a Lie subalgebra of $\mathfrak{gl}(\mathfrak g)$, since the Jacobi identity gives
\begin{align*}
[\operatorname{ad}x,\operatorname{ad}y]=\operatorname{ad}[x,y]
\end{align*}
for all $x,y \in \mathfrak g$.
The same identity identifies the derived algebra of $\mathfrak h$:
\begin{align*}
[\mathfrak h,\mathfrak h]
=
[\operatorname{ad}\mathfrak g,\operatorname{ad}\mathfrak g]
=
\operatorname{ad}[\mathfrak g,\mathfrak g].
\end{align*}
Therefore every element $A \in [\mathfrak h,\mathfrak h]$ has the form $A=\operatorname{ad}x$ for some $x \in [\mathfrak g,\mathfrak g]$, and every element $B \in \mathfrak h$ has the form $B=\operatorname{ad}y$ for some $y \in \mathfrak g$. The assumed vanishing of the Killing form then gives
\begin{align*}
\operatorname{tr}_F(A \circ B)
= \operatorname{tr}_F(\operatorname{ad}x \circ \operatorname{ad}y)
= \kappa(x,y)
=0.
\end{align*}
Thus $\mathfrak h \subseteq \mathfrak{gl}(\mathfrak g)$ satisfies the hypothesis of the Cartan trace criterion for linear Lie algebras (citing a result not yet in the wiki: Cartan Trace Criterion): the trace pairing $\operatorname{tr}_F(A \circ B)$ vanishes whenever $A \in [\mathfrak h,\mathfrak h]$ and $B \in \mathfrak h$. Since $\mathfrak h$ is finite-dimensional over a field of characteristic $0$, the criterion implies that $\mathfrak h$ is solvable.
[/guided]
[/step]
[step:Lift solvability from the adjoint image back to $\mathfrak g$]
The [kernel of the adjoint representation](/theorems/3752) is
\begin{align*}
\ker(\operatorname{ad})
=
\{z \in \mathfrak g : [z,w]=0 \text{ for every } w \in \mathfrak g\}
=
Z(\mathfrak g),
\end{align*}
the center of $\mathfrak g$, which is abelian.
Since $\mathfrak h=\operatorname{ad}\mathfrak g$ is solvable, there exists $m \in \mathbb N$ such that $\mathfrak h^{(m)}=0$, where $\mathfrak h^{(0)}=\mathfrak h$ and $\mathfrak h^{(r+1)}=[\mathfrak h^{(r)},\mathfrak h^{(r)}]$. The homomorphism property of $\operatorname{ad}$ gives
\begin{align*}
\operatorname{ad}(\mathfrak g^{(m)})=\mathfrak h^{(m)}=0,
\end{align*}
so $\mathfrak g^{(m)} \subseteq Z(\mathfrak g)$. Since $Z(\mathfrak g)$ is abelian,
\begin{align*}
\mathfrak g^{(m+1)}
=
[\mathfrak g^{(m)},\mathfrak g^{(m)}]
\subseteq
[Z(\mathfrak g),Z(\mathfrak g)]
=
0.
\end{align*}
Hence the derived series of $\mathfrak g$ terminates, so $\mathfrak g$ is solvable. This proves the converse implication and completes the proof.
[/step]