Iwasawa decomposition on the lie algebra level

$\mathfrak{n}$ is a Lie subalgebra of ${\mathfrak{g}}_0$: if $\lambda ,\mu \in {\mathrm{\Sigma }}^{+}$ then $[{\mathfrak{g}}_0^{\lambda },{\mathfrak{g}}_0^{\mu }]\subseteq {\mathfrak{g}}_0^{\lambda +\mu }$ by [L1], and ${\mathfrak{g}}_0^{\lambda +\mu }=0$ unless $\lambda +\mu \in \mathrm{\Sigma }$, in which case $(\lambda +\mu )(H_0)=\lambda (H_0)+\mu (H_0)>0$ and $\lambda +\mu \in {\mathrm{\Sigma }}^{+}$; hence $[\mathfrak{n},\mathfrak{n}]\subseteq \mathfrak{n}$.

$\mathfrak{n}$ is nilpotent: if ${\mathrm{\Sigma }}^{+}=\mathrm{\varnothing }$ then $\mathfrak{n}=0$ and nilpotency is trivial, so assume ${\mathrm{\Sigma }}^{+}\mathrm{\ne }\mathrm{\varnothing }$; let $m=\min \{\lambda (H_0):\lambda \in {\mathrm{\Sigma }}^{+}\}>0$ and $M=\max \{\lambda (H_0):\lambda \in {\mathrm{\Sigma }}^{+}\}<\mathrm{\infty }$ by [L2]; every iterated bracket of $k$ elements of $\mathfrak{n}$ lies in $⨁{\mathfrak{g}}_0^{{\lambda }_1+\cdots +{\lambda }_k}$ with ${\lambda }_j\in {\mathrm{\Sigma }}^{+}$, and this sum is $0$ unless ${\lambda }_1+\cdots +{\lambda }_k\in \mathrm{\Sigma }\cup \{0\}$; but its value at $H_0$ is at least $km>0$, so it is not $0$ as a functional on the regular element $H_0$, and if it were a restricted root it would lie in ${\mathrm{\Sigma }}^{+}$ and its value at $H_0$ would be at most $M$; hence $km\le M$, so for $k>M\mathrm{/}m$ every iterated bracket of $k$ elements of $\mathfrak{n}$ vanishes and the descending central series of $\mathfrak{n}$ reaches $0$.

${\mathfrak{k}}_0\cap (\mathfrak{a}\oplus \mathfrak{n})=0$: let $X\in {\mathfrak{k}}_0\cap (\mathfrak{a}\oplus \mathfrak{n})$; write $X=H+Y$ with $H\in \mathfrak{a}$ and $Y\in \mathfrak{n}$, and note that $\theta X=X$ while $\theta H=-H$ and $\theta Y\in {⨁}_{\lambda \in {\mathrm{\Sigma }}^{+}}{\mathfrak{g}}_0^{-\lambda }$; hence $\theta X=-H+\theta Y$, and the direct sum decomposition of ${\mathfrak{g}}_0$ into ${\mathfrak{g}}_0^0$ and the restricted-root spaces, applied to the two expressions $X=H+Y$ and $\theta X=-H+\theta Y$ for the same element, gives $H=-H$, that is $H=0$, and $\theta Y=Y$; then $Y\in \mathfrak{n}\cap \theta \mathfrak{n}=0$ by [L1] because the direct sum is over the disjoint sets of positive and negative roots; hence $X=0$, and $X\in {\mathfrak{k}}_0\cap {\mathfrak{p}}_0=0$ by [L3].

${\mathfrak{k}}_0+\mathfrak{a}+\mathfrak{n}={\mathfrak{g}}_0$: let $X\in {\mathfrak{g}}_0$ and write $X=X_0+{\sum }_{\lambda \in \mathrm{\Sigma }}{X}_{\lambda }$ with $X_0\in {\mathfrak{g}}_0^0$ and $X_{\lambda }\in {\mathfrak{g}}_0^{\lambda }$; by [L1] write $X_0=H+X_{\mathfrak{m}}$ with $H\in \mathfrak{a}$ and $X_{\mathfrak{m}}\in \mathfrak{m}\subseteq {\mathfrak{k}}_0$, and put $Z_1=X_{\mathfrak{m}}+{\sum }_{\lambda \in {\mathrm{\Sigma }}^{+}}(X_{-\lambda }+\theta X_{-\lambda })$, $Z_2=H$ and $Z_3={\sum }_{\lambda \in {\mathrm{\Sigma }}^{+}}(X_{\lambda }-\theta X_{-\lambda })$; then $Z_1\in {\mathfrak{k}}_0$ because each $X_{-\lambda }+\theta X_{-\lambda }$ is fixed by $\theta$ and $X_{\mathfrak{m}}\in \mathfrak{m}\subseteq {\mathfrak{k}}_0$ by [L1] and [L3], $Z_2\in \mathfrak{a}$, and $Z_3\in \mathfrak{n}$ because $X_{\lambda }\in {\mathfrak{g}}_0^{\lambda }$ and $\theta X_{-\lambda }\in {\mathfrak{g}}_0^{\lambda }$ by [L1]; since $Z_1+Z_2+Z_3=X$, the sum ${\mathfrak{k}}_0+\mathfrak{a}+\mathfrak{n}$ is all of ${\mathfrak{g}}_0$.

$\mathfrak{a}$ normalizes $\mathfrak{n}$: for $\lambda \in {\mathrm{\Sigma }}^{+}$ and $H\in \mathfrak{a}$ with $\lambda (H)\mathrm{\ne }0$ the map $X\mapsto [H,X]$ on ${\mathfrak{g}}_0^{\lambda }$ is multiplication by the nonzero scalar $\lambda (H)$, hence is surjective onto ${\mathfrak{g}}_0^{\lambda }$; since such $H$ exist and $[H,{\mathfrak{g}}_0^{\lambda }]\subseteq {\mathfrak{g}}_0^{\lambda }$ by [L1], $[\mathfrak{a},{\mathfrak{g}}_0^{\lambda }]={\mathfrak{g}}_0^{\lambda }$ for every $\lambda \in {\mathrm{\Sigma }}^{+}$ and $[\mathfrak{a},\mathfrak{n}]=\mathfrak{n}$; therefore $\mathfrak{a}\oplus \mathfrak{n}$ is a subalgebra with $[\mathfrak{a}\oplus \mathfrak{n},\mathfrak{a}\oplus \mathfrak{n}]=[\mathfrak{a},\mathfrak{n}]+[\mathfrak{n},\mathfrak{n}]=\mathfrak{n}$, since $[\mathfrak{a},\mathfrak{a}]=0$ and $[\mathfrak{n},\mathfrak{n}]\subseteq \mathfrak{n}$.

By steps 1.3 and 1.4 the sum ${\mathfrak{k}}_0+\mathfrak{a}+\mathfrak{n}$ equals ${\mathfrak{g}}_0$ and its intersection in pairs is zero, so ${\mathfrak{g}}_0={\mathfrak{k}}_0\oplus \mathfrak{a}\oplus \mathfrak{n}$ is a direct sum; $\mathfrak{a}$ is abelian by definition, $\mathfrak{n}$ is nilpotent by step 1.2, $\mathfrak{a}\oplus \mathfrak{n}$ is a subalgebra with derived subalgebra $[\mathfrak{a}\oplus \mathfrak{n},\mathfrak{a}\oplus \mathfrak{n}]=\mathfrak{n}$ by step 2.1, and it is solvable because its derived series begins $\mathfrak{a}\oplus \mathfrak{n}\supseteq \mathfrak{n}$ and then coincides with the derived series of the nilpotent algebra $\mathfrak{n}$, which reaches $0$.