[proofplan] We prove the result by induction on $\dim_F \mathfrak g$. If $\mathfrak g$ is already simple, the decomposition has one summand. Otherwise we choose a non-zero proper ideal $\mathfrak a \trianglelefteq \mathfrak g$ and use the orthogonal-complement decomposition theorem for ideals in a semisimple Lie algebra to split $\mathfrak g$ as a direct sum of two smaller commuting semisimple ideals. Applying the induction hypothesis to those two ideals and then viewing the resulting simple summands as ideals of $\mathfrak g$ gives the desired decomposition. [/proofplan]

[step:Start the induction and dispose of the simple case]We argue by induction on the integer $n := \dim_F \mathfrak g$. If $n=0$, then $\mathfrak g=0$ and the assertion holds with $m=0$, where the right-hand side is the empty direct sum. If $n>0$ and $\mathfrak g$ is simple, then the assertion holds with $m=1$ and $\mathfrak g_1 := \mathfrak g$. It remains to consider the case in which $\mathfrak g$ is non-zero, semisimple, and not simple. Then there exists a non-zero proper ideal $\mathfrak a \trianglelefteq \mathfrak g$.[/step]

[guided]The induction parameter is the finite dimension \begin{align*} n := \dim_F \mathfrak g. \end{align*} This is well-defined because $\mathfrak g$ is finite-dimensional over $F$ by hypothesis. There are two terminal cases. First, if $n=0$, then $\mathfrak g=0$. The statement allows $m=0$, and the empty direct sum is $0$, so the result holds. Second, suppose $n>0$ and $\mathfrak g$ is simple. By definition, a simple Lie algebra is non-zero and has no non-zero proper ideals. In this case we take \begin{align*} m := 1, \qquad \mathfrak g_1 := \mathfrak g. \end{align*} Then $\mathfrak g_1$ is a simple ideal of $\mathfrak g$, and \begin{align*} \mathfrak g = \mathfrak g_1. \end{align*} There are no distinct indices $i,j$ to check for the commutation condition. Thus the only remaining case is that $\mathfrak g$ is non-zero, semisimple, and not simple. Since it is not simple, there exists a non-zero proper ideal \begin{align*} \mathfrak a \trianglelefteq \mathfrak g, \qquad 0 \neq \mathfrak a \neq \mathfrak g. \end{align*} This ideal is the object to which we apply the splitting theorem in the next step.[/guided]

[step:Split off a commuting semisimple complementary ideal]Let $\kappa_{\mathfrak g}: \mathfrak g \times \mathfrak g \to F$ denote the Killing form of $\mathfrak g$, and define the orthogonal complement of $\mathfrak a$ in $\mathfrak g$ by \begin{align*} \mathfrak a^\perp := \{x \in \mathfrak g : \kappa_{\mathfrak g}(x,y)=0 \text{ for every } y \in \mathfrak a\}. \end{align*} By the orthogonal-complement theorem for ideals in semisimple Lie algebras (citing a result not yet in the wiki: Orthogonal Complement Theorem for Ideals in Semisimple Lie Algebras), $\mathfrak a^\perp$ is an ideal of $\mathfrak g$ and \begin{align*} \mathfrak g = \mathfrak a \oplus \mathfrak a^\perp, \qquad [\mathfrak a,\mathfrak a^\perp]=0. \end{align*} Since $\mathfrak a$ is non-zero and proper, this direct-sum decomposition implies \begin{align*} 0 < \dim_F \mathfrak a < \dim_F \mathfrak g, \qquad 0 < \dim_F \mathfrak a^\perp < \dim_F \mathfrak g. \end{align*}[/step]

[guided]We use the Killing form to produce the complementary ideal. Let \begin{align*} \kappa_{\mathfrak g}: \mathfrak g \times \mathfrak g &\to F \end{align*} be the Killing form of $\mathfrak g$. For the chosen ideal $\mathfrak a \trianglelefteq \mathfrak g$, define its Killing-orthogonal complement by \begin{align*} \mathfrak a^\perp := \{x \in \mathfrak g : \kappa_{\mathfrak g}(x,y)=0 \text{ for every } y \in \mathfrak a\}. \end{align*} The relevant structural input is the orthogonal-complement theorem for ideals in semisimple Lie algebras (citing a result not yet in the wiki: Orthogonal Complement Theorem for Ideals in Semisimple Lie Algebras). Its hypotheses are satisfied here: $F$ has characteristic $0$, $\mathfrak g$ is finite-dimensional and semisimple over $F$, and $\mathfrak a$ is an ideal of $\mathfrak g$. Therefore the theorem gives three conclusions: \begin{align*} \mathfrak a^\perp \trianglelefteq \mathfrak g, \qquad \mathfrak g = \mathfrak a \oplus \mathfrak a^\perp, \qquad [\mathfrak a,\mathfrak a^\perp]=0. \end{align*} The direct sum is crucial for induction because it makes both summands strictly smaller. Since $\mathfrak a \neq 0$, we have $\dim_F \mathfrak a>0$. Since $\mathfrak a \neq \mathfrak g$ and \begin{align*} \mathfrak g = \mathfrak a \oplus \mathfrak a^\perp, \end{align*} the complement $\mathfrak a^\perp$ is non-zero. Also both summands are proper subspaces of $\mathfrak g$, so \begin{align*} 0 < \dim_F \mathfrak a < \dim_F \mathfrak g, \qquad 0 < \dim_F \mathfrak a^\perp < \dim_F \mathfrak g. \end{align*} Thus both summands fall within the induction range.[/guided]

[step:Verify that both summands are semisimple]We show that $\mathfrak a$ is semisimple; the same argument applies to $\mathfrak a^\perp$. Let $\mathfrak r \trianglelefteq \mathfrak a$ be a solvable ideal of the Lie algebra $\mathfrak a$. For every $x \in \mathfrak g$, write uniquely \begin{align*} x = y + z, \qquad y \in \mathfrak a, \qquad z \in \mathfrak a^\perp. \end{align*} Since $\mathfrak r \trianglelefteq \mathfrak a$, we have $[y,\mathfrak r]\subseteq \mathfrak r$. Since $[\mathfrak a^\perp,\mathfrak a]=0$ and $\mathfrak r \subseteq \mathfrak a$, we have $[z,\mathfrak r]=0$. Therefore \begin{align*} [x,\mathfrak r] = [y+z,\mathfrak r] \subseteq [y,\mathfrak r]+[z,\mathfrak r] \subseteq \mathfrak r. \end{align*} Hence $\mathfrak r \trianglelefteq \mathfrak g$. Because $\mathfrak r$ is solvable and $\mathfrak g$ is semisimple, $\mathfrak r=0$. Thus $\mathfrak a$ has no non-zero solvable ideals, so $\mathfrak a$ is semisimple. The same proof with $\mathfrak a$ and $\mathfrak a^\perp$ interchanged shows that $\mathfrak a^\perp$ is semisimple.[/step]

[guided]We now need to justify that induction applies not just dimensionally, but also structurally: the summands must themselves be semisimple Lie algebras. We prove this for $\mathfrak a$. Let \begin{align*} \mathfrak r \trianglelefteq \mathfrak a \end{align*} be a solvable ideal of the Lie algebra $\mathfrak a$. To prove that $\mathfrak a$ is semisimple, we must show $\mathfrak r=0$. The point is that $\mathfrak r$ is automatically an ideal of the larger Lie algebra $\mathfrak g$. Let $x \in \mathfrak g$. Since \begin{align*} \mathfrak g = \mathfrak a \oplus \mathfrak a^\perp, \end{align*} there exist unique elements $y \in \mathfrak a$ and $z \in \mathfrak a^\perp$ such that \begin{align*} x = y+z. \end{align*} Because $\mathfrak r$ is an ideal of $\mathfrak a$, the bracket of $y$ with $\mathfrak r$ stays inside $\mathfrak r$: \begin{align*} [y,\mathfrak r]\subseteq \mathfrak r. \end{align*} Because the two summands commute and $\mathfrak r \subseteq \mathfrak a$, we also have \begin{align*} [z,\mathfrak r]=0. \end{align*} Combining these two facts gives \begin{align*} [x,\mathfrak r] = [y+z,\mathfrak r] \subseteq [y,\mathfrak r]+[z,\mathfrak r] \subseteq \mathfrak r. \end{align*} Thus $\mathfrak r \trianglelefteq \mathfrak g$. Now $\mathfrak r$ is a solvable ideal of $\mathfrak g$. Since $\mathfrak g$ is semisimple, it has no non-zero solvable ideals. Therefore $\mathfrak r=0$. This proves that $\mathfrak a$ is semisimple. The same argument applies to $\mathfrak a^\perp$: if $\mathfrak s \trianglelefteq \mathfrak a^\perp$ is solvable, then the decomposition \begin{align*} \mathfrak g = \mathfrak a \oplus \mathfrak a^\perp \end{align*} and the commutation relation $[\mathfrak a,\mathfrak a^\perp]=0$ imply $\mathfrak s \trianglelefteq \mathfrak g$, hence $\mathfrak s=0$. Therefore $\mathfrak a^\perp$ is semisimple.[/guided]

[step:Apply induction to the two smaller semisimple ideals]By the induction hypothesis applied to $\mathfrak a$, there exist simple ideals \begin{align*} \mathfrak a_1,\dots,\mathfrak a_p \trianglelefteq \mathfrak a \end{align*} such that \begin{align*} \mathfrak a = \mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p, \qquad [\mathfrak a_i,\mathfrak a_j]=0 \quad \text{for } i\neq j. \end{align*} By the induction hypothesis applied to $\mathfrak a^\perp$, there exist simple ideals \begin{align*} \mathfrak b_1,\dots,\mathfrak b_q \trianglelefteq \mathfrak a^\perp \end{align*} such that \begin{align*} \mathfrak a^\perp = \mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q, \qquad [\mathfrak b_i,\mathfrak b_j]=0 \quad \text{for } i\neq j. \end{align*} Since each $\mathfrak a_i$ is an ideal of $\mathfrak a$ and $[\mathfrak a^\perp,\mathfrak a]=0$, each $\mathfrak a_i$ is an ideal of $\mathfrak g$. Likewise, each $\mathfrak b_j$ is an ideal of $\mathfrak g$.[/step]

[guided]Both $\mathfrak a$ and $\mathfrak a^\perp$ are finite-dimensional semisimple Lie algebras over $F$, and both have dimension strictly smaller than $\dim_F \mathfrak g$. Therefore the induction hypothesis applies to each one. Applied to $\mathfrak a$, the induction hypothesis gives simple ideals \begin{align*} \mathfrak a_1,\dots,\mathfrak a_p \trianglelefteq \mathfrak a \end{align*} such that \begin{align*} \mathfrak a = \mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p, \qquad [\mathfrak a_i,\mathfrak a_j]=0 \quad \text{whenever } i\neq j. \end{align*} Applied to $\mathfrak a^\perp$, it gives simple ideals \begin{align*} \mathfrak b_1,\dots,\mathfrak b_q \trianglelefteq \mathfrak a^\perp \end{align*} such that \begin{align*} \mathfrak a^\perp = \mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q, \qquad [\mathfrak b_i,\mathfrak b_j]=0 \quad \text{whenever } i\neq j. \end{align*} We must still check that these summands are ideals of $\mathfrak g$, not only ideals of the smaller summands. Let $u \in \mathfrak a_i$ and let $x \in \mathfrak g$. Write $x=y+z$ with $y \in \mathfrak a$ and $z \in \mathfrak a^\perp$. Since $\mathfrak a_i \trianglelefteq \mathfrak a$, \begin{align*} [y,u]\in \mathfrak a_i. \end{align*} Since $[\mathfrak a^\perp,\mathfrak a]=0$ and $u \in \mathfrak a$, we have \begin{align*} [z,u]=0. \end{align*} Therefore \begin{align*} [x,u]=[y+z,u]=[y,u]+[z,u]\in \mathfrak a_i. \end{align*} Thus $\mathfrak a_i \trianglelefteq \mathfrak g$. The same argument, with $\mathfrak a$ and $\mathfrak a^\perp$ interchanged, shows that each $\mathfrak b_j \trianglelefteq \mathfrak g$.[/guided]

[step:Assemble the simple ideals and verify pairwise commutation] Set \begin{align*} m := p+q \end{align*} and list the ideals \begin{align*} \mathfrak g_1,\dots,\mathfrak g_m \end{align*} as \begin{align*} \mathfrak a_1,\dots,\mathfrak a_p,\mathfrak b_1,\dots,\mathfrak b_q. \end{align*} Using the two direct-sum decompositions and $\mathfrak g=\mathfrak a\oplus\mathfrak a^\perp$, we obtain \begin{align*} \mathfrak g &= \mathfrak a \oplus \mathfrak a^\perp \\ &= (\mathfrak a_1 \oplus \cdots \oplus \mathfrak a_p) \oplus (\mathfrak b_1 \oplus \cdots \oplus \mathfrak b_q) \\ &= \mathfrak g_1 \oplus \cdots \oplus \mathfrak g_m. \end{align*} The summands are simple ideals of $\mathfrak g$ by the previous step. Ideals from the same family commute by the induction hypothesis, and ideals from different families commute because \begin{align*} [\mathfrak a,\mathfrak a^\perp]=0. \end{align*} Hence $[\mathfrak g_i,\mathfrak g_j]=0$ for every $i\neq j$. This completes the induction and the proof. [/step]