The roots form a reduced crystallographic Euclidean root system

By [L1] and [L2], $\mathrm{\Phi }$ is finite, $\dim {\mathfrak{g}}_{\alpha }=1$ for every $\alpha \in \mathrm{\Phi }$, and $\mathfrak{g}=\mathfrak{h}\oplus {⨁}_{\alpha \in \mathrm{\Phi }}{\mathfrak{g}}_{\alpha }$ with $\mathfrak{h}={\mathfrak{g}}_0$ the zero eigenspace; hence for $H\in \mathfrak{h}$ the operator ${\mathrm{ad}}_H$ is diagonalisable on $\mathfrak{g}$ with eigenvalues $\alpha (H)$, each occurring on the one-dimensional space ${\mathfrak{g}}_{\alpha }$, together with the eigenvalue $0$ on $\mathfrak{h}$.

The roots span ${\mathfrak{h}}^{\ast }$ over $\mathbb{C}$: a proper subspace of ${\mathfrak{h}}^{\ast }$ has nonzero annihilator in $\mathfrak{h}$, so if $\mathrm{\Phi }$ did not span ${\mathfrak{h}}^{\ast }$ there would be $0\mathrm{\ne }H\in \mathfrak{h}$ with $\alpha (H)=0$ for every $\alpha$, contradicting [L2].

Fix $\alpha \in \mathrm{\Phi }$ and put $c=\alpha (H_{\alpha })=B(H_{\alpha },H_{\alpha })\mathrm{\ne }0$. Since $H_{\alpha }=(c\mathrm{/}2)h_{\alpha }$, [L4] gives $\beta (H_{\alpha })=(c\mathrm{/}2)\beta (h_{\alpha })$ for every root $\beta$. Applying the trace formula of [L5] to $H_{\alpha }$ and using step 1.1 yields $c=B(H_{\alpha },H_{\alpha })={\sum }_{\beta \in \mathrm{\Phi }}\beta (H_{\alpha }{)}^2=\frac{c^2}{4}{\sum }_{\beta \in \mathrm{\Phi }}\beta (h_{\alpha }{)}^2\mathrm{.}$ The final sum is a positive integer because it contains the term $\alpha (h_{\alpha }{)}^2=4$; division by $c\mathrm{\ne }0$ therefore gives $c=\frac{4}{{\sum }_{\beta \in \mathrm{\Phi }}\beta (h_{\alpha }{)}^2}>0.$ Thus $h_{\alpha }=(2\mathrm{/}c)H_{\alpha }$ is a nonzero real multiple of $H_{\alpha }$.

By [L3] the map $\phi :{\mathfrak{h}}^{\ast }\to \mathfrak{h}$, $\phi (\lambda )=H_{\lambda }$ with $B(H_{\lambda },H)=\lambda (H)$ for all $H\in \mathfrak{h}$, is a $\mathbb{C}$-linear isomorphism; since the $H_{\alpha }$ are the images of the roots, step 1.2 shows that $\{H_{\alpha }:\alpha \in \mathrm{\Phi }\}$ spans $\mathfrak{h}$ over $\mathbb{C}$, and step 2.1 shows that the coroots $h_{\alpha }$ have the same complex span. Hence ${\mathfrak{h}}_{\mathbb{R}}$ spans $\mathfrak{h}$ over $\mathbb{C}$.

Every $\alpha \in \mathrm{\Phi }$ is real valued on ${\mathfrak{h}}_{\mathbb{R}}$, because a real linear combination $H={\sum }_{\beta }{c}_{\beta }{h}_{\beta }$ of coroots satisfies $\alpha (H)={\sum }_{\beta }{c}_{\beta }\alpha (h_{\beta })\in \mathbb{R}$ by [L4]; consequently, for $H\in {\mathfrak{h}}_{\mathbb{R}}$, [L5] and step 1.1 give $B(H,H)=\mathrm{tr}({\mathrm{ad}}_H^2)={\sum }_{\alpha \in \mathrm{\Phi }}\alpha (H{)}^2\ge 0$, and if $B(H,H)=0$ then $\alpha (H)=0$ for all $\alpha$, so $H=0$ by [L2]; thus $B{\mathrm{\mid }}_{{\mathfrak{h}}_{\mathbb{R}}}$ is positive definite.

The form $B{\mathrm{\mid }}_{{\mathfrak{h}}_{\mathbb{R}}}$ is positive definite by step 4.1; in particular ${\mathfrak{h}}_{\mathbb{R}}\cap i{\mathfrak{h}}_{\mathbb{R}}=0$, because a vector in the intersection has $\alpha (H)\in \mathbb{R}\cap i\mathbb{R}=\{0\}$ for every root by step 4.1 and then $H=0$ by [L2]; moreover ${\mathfrak{h}}_{\mathbb{R}}+i{\mathfrak{h}}_{\mathbb{R}}$ is a $\mathbb{C}$-subspace of $\mathfrak{h}$ containing the spanning set ${\mathfrak{h}}_{\mathbb{R}}$ of step 3.1, hence equals $\mathfrak{h}$, so $\mathfrak{h}={\mathfrak{h}}_{\mathbb{R}}\oplus i{\mathfrak{h}}_{\mathbb{R}}$ and ${\dim }_{\mathbb{R}}{\mathfrak{h}}_{\mathbb{R}}={\dim }_{\mathbb{C}}\mathfrak{h}$.

Let $\lambda \in E={\mathrm{span}}_{\mathbb{R}}\mathrm{\Phi }$, say $\lambda ={\sum }_{\alpha }{c}_{\alpha }\alpha$ with real $c_{\alpha }$; then $\lambda (H)\in \mathbb{R}$ for every $H\in {\mathfrak{h}}_{\mathbb{R}}$ by step 4.1, so restriction is a real linear map $E\to {\mathrm{Hom}}_{\mathbb{R}}({\mathfrak{h}}_{\mathbb{R}},\mathbb{R})$, and it is injective because a functional vanishing on ${\mathfrak{h}}_{\mathbb{R}}$ vanishes on the $\mathbb{C}$-span of ${\mathfrak{h}}_{\mathbb{R}}$, which is $\mathfrak{h}$ by step 5.1; since ${\dim }_{\mathbb{R}}E\ge {\dim }_{\mathbb{C}}{\mathfrak{h}}^{\ast }={\dim }_{\mathbb{C}}\mathfrak{h}={\dim }_{\mathbb{R}}{\mathfrak{h}}_{\mathbb{R}}={\dim }_{\mathbb{R}}{\mathrm{Hom}}_{\mathbb{R}}({\mathfrak{h}}_{\mathbb{R}},\mathbb{R})$ by [L2] and step 5.1, the injection is an isomorphism, and $\mathrm{\Phi }$ spans the real space $E$. This proves (i).

For $\lambda ,\mu \in E$ define $(\lambda ,\mu ):=B(H_{\lambda },H_{\mu })$, where $H_{\lambda }\in {\mathfrak{h}}_{\mathbb{R}}$ is characterised by $B(H_{\lambda },H)=\lambda (H)$ for all $H\in {\mathfrak{h}}_{\mathbb{R}}$; this is bilinear, symmetric and positive definite by step 4.1, so it is an inner product on $E$. This proves the first assertion of (iii).

For roots $\alpha ,\beta$ we have $H_{\alpha }\in {\mathfrak{h}}_{\mathbb{R}}$ and $\frac{2(\beta ,\alpha )}{(\alpha ,\alpha )}=\frac{2B(H_{\beta },H_{\alpha })}{B(H_{\alpha },H_{\alpha })}=\frac{2\beta (H_{\alpha })}{\alpha (H_{\alpha })}=\beta (\frac{2H_{\alpha }}{\alpha (H_{\alpha })})=\beta (h_{\alpha })\in \mathbb{Z}$ by [L3], [L4] and step 7.1; this is the crystallographic identity in (iii), and it identifies the abstract reflection $x\mapsto x-\frac{2(x,\alpha )}{(\alpha ,\alpha )}\alpha$ with $s_{\alpha }(x)=x-x(h_{\alpha })\alpha$ of [L6].

The set $\mathrm{\Phi }\subseteq E$ is finite, consists of nonzero vectors and spans $E$ by step 6.1; the reflection identity of step 8.1 shows that $s_{\alpha }(\mathrm{\Phi })\subseteq \mathrm{\Phi }$ for every $\alpha$, because $s_{\alpha }(\beta )$ is a root for all roots $\beta$ by [L6] and $s_{\alpha }$ is involutive, so $s_{\alpha }(\mathrm{\Phi })=\mathrm{\Phi }$; the crystallographic integrality condition is step 8.1; and reducedness holds because the only scalar multiples of a root that are roots are $\alpha$ and $-\alpha$, both of which lie in $\mathrm{\Phi }$, by [L6]; hence $(E,\mathrm{\Phi })$ is a reduced crystallographic Euclidean root system whose reflections are exactly the reflections $s_{\alpha }$ of [L6]. This proves (iv).

Let $\mathrm{\Delta }=\{{\alpha }_1,\dots ,{\alpha }_r\}$ be the base of a positive system of $(E,\mathrm{\Phi })$; by [L7] it is a basis of $E$, so under the isomorphism $E\to {\mathfrak{h}}_{\mathbb{R}}$, $\lambda \mapsto H_{\lambda }$, of step 6.1 the vectors $H_{{\alpha }_1},\dots ,H_{{\alpha }_r}$ form a basis of ${\mathfrak{h}}_{\mathbb{R}}$, and since $h_{{\alpha }_i}$ is a nonzero real multiple of $H_{{\alpha }_i}$ by [L3], the coroots $h_{{\alpha }_1},\dots ,h_{{\alpha }_r}$ also form a basis of ${\mathfrak{h}}_{\mathbb{R}}$; because $\mathfrak{h}={\mathfrak{h}}_{\mathbb{R}}\oplus i{\mathfrak{h}}_{\mathbb{R}}$ by step 5.1, that basis is a $\mathbb{C}$-basis of $\mathfrak{h}$ as well, which proves (v) and completes the proof.