[proofplan]
We verify the axioms of an abstract crystallographic root system one by one. Finiteness, non-vanishing, spanning, and positive definiteness come from the root space decomposition and the Killing-form construction of the real root space. The [root string theorem](/theorems/4693) supplies both the integrality of Cartan integers and the reflection formula $s_\alpha(\beta) \in \Phi$. Finally, the no-double-roots theorem excludes the only possible nontrivial scalar multiples, giving reducedness.
[/proofplan]
[step:Construct the real root space and record the induced positive definite form]
Let $\kappa: \mathfrak g \times \mathfrak g \to k$ denote the Killing form of $\mathfrak g$. Since $\mathfrak g$ is semisimple, $\kappa$ is nondegenerate on $\mathfrak g$, and its restriction to the Cartan subalgebra $\mathfrak h$ is nondegenerate. Thus for each $\lambda \in \mathfrak h^*$ there is a unique element $t_\lambda \in \mathfrak h$ such that
\begin{align*}
\lambda(H) = \kappa(t_\lambda,H)
\end{align*}
for every $H \in \mathfrak h$.
Define a symmetric bilinear pairing on $\mathfrak h^*$ by
\begin{align*}
(\lambda,\mu) := \kappa(t_\lambda,t_\mu)
\end{align*}
for $\lambda,\mu \in \mathfrak h^*$. Let
\begin{align*}
E := \operatorname{span}_{\mathbb R}\Phi
\end{align*}
be the real [vector space](/page/Vector%20Space) generated by the roots. We now invoke the [positivity of the Killing form on the real root span](/theorems/4102). Its hypotheses are exactly the hypotheses in force here: $\mathfrak g$ is finite-dimensional and semisimple, $k$ is algebraically closed of characteristic zero, $\mathfrak h$ is a [Cartan subalgebra](/page/Cartan%20Subalgebra), and $\Phi$ is the set of nonzero roots in the [root space decomposition](/page/Root%20Space%20Decomposition). The theorem states that the pairing transferred from the [Killing form](/page/Killing%20Form) by the representatives $t_\lambda$ is real-valued and positive definite on $E=\operatorname{span}_{\mathbb R}\Phi$, and that for every root $\alpha$ the associated coroot element $h_\alpha\in\mathfrak h$ satisfies
\begin{align*}
\beta(h_\alpha)=\frac{2(\beta,\alpha)}{(\alpha,\alpha)}
\end{align*}
for every $\beta\in\Phi$. Thus $(E,(\cdot,\cdot))$ is a finite-dimensional Euclidean vector space, and the normalization used below agrees with the root-string normalization.
[guided]
The Killing form gives the inner product used in the root system. Because $\mathfrak g$ is semisimple, the Killing form
\begin{align*}
\kappa: \mathfrak g \times \mathfrak g \to k
\end{align*}
is nondegenerate. Its restriction to the Cartan subalgebra $\mathfrak h$ is also nondegenerate, so every linear functional $\lambda \in \mathfrak h^*$ is represented uniquely by an element $t_\lambda \in \mathfrak h$ satisfying
\begin{align*}
\lambda(H) = \kappa(t_\lambda,H)
\end{align*}
for all $H \in \mathfrak h$.
This lets us transfer the Killing form from $\mathfrak h$ to $\mathfrak h^*$ by defining
\begin{align*}
(\lambda,\mu) := \kappa(t_\lambda,t_\mu).
\end{align*}
The theorem concerns only the real span of the roots, so we set
\begin{align*}
E := \operatorname{span}_{\mathbb R}\Phi.
\end{align*}
At this point we use the [positivity of the Killing form on the real root span](/theorems/4102). The theorem applies because $\mathfrak g$ is finite-dimensional and semisimple, the field $k$ is algebraically closed of characteristic zero, and $\mathfrak h$ is a [Cartan subalgebra](/page/Cartan%20Subalgebra). It gives two facts at once. First, the transferred Killing-form pairing is real-valued and positive definite on
\begin{align*}
E=\operatorname{span}_{\mathbb R}\Phi.
\end{align*}
Second, if $h_\alpha\in\mathfrak h$ denotes the coroot element associated to a root $\alpha$, then the Killing-form normalization and the Lie-algebraic coroot normalization agree:
\begin{align*}
\beta(h_\alpha)=\frac{2(\beta,\alpha)}{(\alpha,
\alpha)}
\end{align*}
for every root $\beta\in\Phi$.
This second point is essential. The root-string theorem below computes the integer $\beta(h_\alpha)$ from the embedded $\mathfrak{sl}_2$-structure, while the abstract root system axiom is written using the Euclidean formula $2(\beta,\alpha)/(\alpha,\alpha)$. The cited positivity theorem identifies these two quantities, so the integrality and reflection formulas obtained from root strings are statements about the same pairing that makes $E$ Euclidean. In particular $(\alpha,\alpha)>0$ for every root $\alpha\in\Phi$, so the reflection formula used below is meaningful.
[/guided]
[/step]
[step:Verify finiteness, nonzero roots, and spanning]
The [root space decomposition](/page/Root%20Space%20Decomposition) relative to $\mathfrak h$ is
\begin{align*}
\mathfrak g = \mathfrak h \oplus \bigoplus_{\alpha \in \Phi} \mathfrak g_\alpha,
\end{align*}
where
\begin{align*}
\mathfrak g_\alpha := \{X \in \mathfrak g : [H,X] = \alpha(H)X \text{ for every } H \in \mathfrak h\}.
\end{align*}
Since $\mathfrak g$ is finite-dimensional, only finitely many nonzero root spaces can occur, so $\Phi$ is finite. By definition $\Phi \subset \mathfrak h^* \setminus \{0\}$, so $0 \notin \Phi$. Since $E$ was defined as $\operatorname{span}_{\mathbb R}\Phi$, the set $\Phi$ spans $E$.
[/step]
[step:Use root strings to obtain integrality and reflection invariance]
Fix $\alpha,\beta \in \Phi$. Define the coroot functional $\alpha^\vee \in E^*$ by
\begin{align*}
\alpha^\vee(\gamma) := \frac{2(\gamma,\alpha)}{(\alpha,\alpha)}
\end{align*}
for $\gamma \in E$, and write
\begin{align*}
\langle \gamma,\alpha^\vee\rangle := \alpha^\vee(\gamma).
\end{align*}
The [Root String Theorem for Semisimple Lie Algebras](/theorems/4103) applies to the roots $\alpha,\beta\in\Phi$ because $\mathfrak g$ is finite-dimensional semisimple over an algebraically closed field of characteristic zero and $\mathfrak h$ is a Cartan subalgebra. It says that the $\alpha$-string through $\beta$ has the form
\begin{align*}
\{\beta - p\alpha,\beta-(p-1)\alpha,\dots,\beta+q\alpha\}
\end{align*}
for some integers $p,q \geq 0$, and that
\begin{align*}
\langle \beta,\alpha^\vee\rangle = p-q.
\end{align*}
Therefore
\begin{align*}
\frac{2(\beta,\alpha)}{(\alpha,\alpha)}
= \langle \beta,\alpha^\vee\rangle
= p-q
\in \mathbb Z.
\end{align*}
This proves the crystallographic integrality condition.
The [Reflection Theorem for Roots](/theorems/4104), applied with the same hypotheses, implies that the reflected root
\begin{align*}
s_\alpha(\beta)
:= \beta - \langle \beta,\alpha^\vee\rangle \alpha
\end{align*}
belongs to $\Phi$. Since $\beta \in \Phi$ was arbitrary, $s_\alpha(\Phi) \subseteq \Phi$. Also $s_\alpha$ is an involution because
\begin{align*}
s_\alpha(s_\alpha(\gamma)) = \gamma
\end{align*}
for every $\gamma \in E$. Hence $s_\alpha(\Phi)=\Phi$.
Here we are citing results not yet resolved to wiki IDs: Root String Theorem for semisimple Lie algebras and Reflection Theorem for roots.
[guided]
Now we prove the two structural properties that make the finite set of roots into a crystallographic reflection system.
Fix roots $\alpha,\beta \in \Phi$. Since $(\alpha,\alpha)>0$, we may define the coroot functional
\begin{align*}
\alpha^\vee: E &\to \mathbb R,\\
\gamma &\mapsto \frac{2(\gamma,\alpha)}{(\alpha,\alpha)}.
\end{align*}
We write $\langle \gamma,\alpha^\vee\rangle := \alpha^\vee(\gamma)$.
The [Root String Theorem for Semisimple Lie Algebras](/theorems/4103) describes all roots of the form $\beta+n\alpha$, where $n \in \mathbb Z$. The theorem applies because $\mathfrak g$ is finite-dimensional semisimple over an algebraically closed field of characteristic zero, $\mathfrak h$ is a Cartan subalgebra, and $\alpha,\beta$ are roots. It says that there are integers $p,q \geq 0$ such that the entire string is
\begin{align*}
\{\beta - p\alpha,\beta-(p-1)\alpha,\dots,\beta+q\alpha\},
\end{align*}
and that the Cartan integer is the difference
\begin{align*}
\langle \beta,\alpha^\vee\rangle = p-q.
\end{align*}
Because $p$ and $q$ are integers, this immediately gives
\begin{align*}
\frac{2(\beta,\alpha)}{(\alpha,\alpha)}
= \langle \beta,\alpha^\vee\rangle
= p-q
\in \mathbb Z.
\end{align*}
This is exactly the crystallographic integrality axiom.
The reflection associated to $\alpha$ is the map
\begin{align*}
s_\alpha: E &\to E,\\
\gamma &\mapsto \gamma-\langle \gamma,\alpha^\vee\rangle\alpha.
\end{align*}
For $\gamma=\beta$, the [Reflection Theorem for Roots](/theorems/4104) says that
\begin{align*}
s_\alpha(\beta)=\beta-\langle\beta,\alpha^\vee\rangle\alpha
\end{align*}
is again a root. Hence $s_\alpha(\beta)\in\Phi$. Since $\beta$ was arbitrary, $s_\alpha(\Phi)\subseteq \Phi$.
Finally, $s_\alpha$ is its own inverse. Indeed, for every $\gamma \in E$,
\begin{align*}
s_\alpha(s_\alpha(\gamma))
&= s_\alpha(\gamma-\langle\gamma,\alpha^\vee\rangle\alpha)\\
&= \gamma-\langle\gamma,\alpha^\vee\rangle\alpha
-\left\langle \gamma-\langle\gamma,\alpha^\vee\rangle\alpha,\alpha^\vee\right\rangle\alpha\\
&= \gamma-\langle\gamma,\alpha^\vee\rangle\alpha
-\left(\langle\gamma,\alpha^\vee\rangle-\langle\gamma,\alpha^\vee\rangle\langle\alpha,\alpha^\vee\rangle\right)\alpha.
\end{align*}
Since
\begin{align*}
\langle\alpha,\alpha^\vee\rangle
= \frac{2(\alpha,\alpha)}{(\alpha,\alpha)}
=2,
\end{align*}
we get
\begin{align*}
s_\alpha(s_\alpha(\gamma))
&= \gamma-\langle\gamma,\alpha^\vee\rangle\alpha
-\left(\langle\gamma,\alpha^\vee\rangle-2\langle\gamma,\alpha^\vee\rangle\right)\alpha\\
&= \gamma.
\end{align*}
Thus $s_\alpha$ is bijective, and $s_\alpha(\Phi)\subseteq\Phi$ implies $s_\alpha(\Phi)=\Phi$.
Here we are citing results not yet resolved to wiki IDs: Root String Theorem for semisimple Lie algebras and Reflection Theorem for roots.
[/guided]
[/step]
[step:Exclude nontrivial scalar multiples of roots]
Let $\alpha \in \Phi$ and suppose $c\alpha \in \Phi$ for some $c \in \mathbb R$. Since $c\alpha \neq 0$, we have $c \neq 0$. Applying the integrality condition to the pair $(c\alpha,\alpha)$ gives
\begin{align*}
\langle c\alpha,\alpha^\vee\rangle
= \frac{2(c\alpha,\alpha)}{(\alpha,\alpha)}
= 2c
\in \mathbb Z.
\end{align*}
Applying the integrality condition to the pair $(\alpha,c\alpha)$ gives
\begin{align*}
\langle \alpha,(c\alpha)^\vee\rangle
= \frac{2(\alpha,c\alpha)}{(c\alpha,c\alpha)}
= \frac{2c(\alpha,\alpha)}{c^2(\alpha,\alpha)}
= \frac{2}{c}
\in \mathbb Z.
\end{align*}
Thus $2c \in \mathbb Z$ and $2/c \in \mathbb Z$. Hence
\begin{align*}
c \in \left\{\pm 1,\pm 2,\pm \frac{1}{2}\right\}.
\end{align*}
The [No Double Roots Theorem for Semisimple Lie Algebras](/theorems/4105) applies because $\mathfrak g$ is finite-dimensional semisimple over an algebraically closed field of characteristic zero and $\Phi$ is its nonzero root set relative to $\mathfrak h$. It states that if $\gamma \in \Phi$, then $2\gamma \notin \Phi$ and $-2\gamma \notin \Phi$. If $c=\pm2$, this contradicts the theorem with $\gamma=\alpha$. If $c=\pm\frac12$, then $\alpha = \pm 2(c\alpha)$, contradicting the theorem with $\gamma=c\alpha$. Therefore $c=\pm1$.
[guided]
Reducedness means that a root line contains only the two opposite roots. So let $\alpha \in \Phi$ and suppose another root lies on the same real line:
\begin{align*}
c\alpha \in \Phi
\end{align*}
for some $c \in \mathbb R$. Since roots are nonzero, $c\alpha \neq 0$, and therefore $c \neq 0$.
We use the crystallographic integrality already proved. First apply it to the ordered pair $(c\alpha,\alpha)$. The coroot functional $\alpha^\vee$ gives
\begin{align*}
\langle c\alpha,\alpha^\vee\rangle
&= \frac{2(c\alpha,\alpha)}{(\alpha,\alpha)}\\
&= 2c.
\end{align*}
Because this Cartan integer must be integral, $2c \in \mathbb Z$.
Now apply the same condition to the ordered pair $(\alpha,c\alpha)$. Since the coroot of $c\alpha$ is defined by the same formula, we have
\begin{align*}
\langle \alpha,(c\alpha)^\vee\rangle
&= \frac{2(\alpha,c\alpha)}{(c\alpha,c\alpha)}\\
&= \frac{2c(\alpha,\alpha)}{c^2(\alpha,\alpha)}\\
&= \frac{2}{c}.
\end{align*}
Thus $2/c \in \mathbb Z$.
The simultaneous conditions
\begin{align*}
2c \in \mathbb Z,
\qquad
\frac{2}{c} \in \mathbb Z
\end{align*}
force
\begin{align*}
c \in \left\{\pm 1,\pm 2,\pm \frac{1}{2}\right\}.
\end{align*}
Indeed, writing $m=2c$ and $n=2/c$, we have $mn=4$, so $m,n \in \mathbb Z$ are nonzero divisors of $4$.
It remains to exclude the four non-unit possibilities. The [No Double Roots Theorem for Semisimple Lie Algebras](/theorems/4105) applies because $\mathfrak g$ is finite-dimensional semisimple over an algebraically closed field of characteristic zero and $\Phi$ is its nonzero root set relative to the Cartan subalgebra $\mathfrak h$. It says that if $\gamma \in \Phi$, then neither $2\gamma$ nor $-2\gamma$ is a root. If $c=2$ or $c=-2$, then $c\alpha=\pm2\alpha$ is a root, contradicting that theorem with $\gamma=\alpha$. If $c=1/2$ or $c=-1/2$, then
\begin{align*}
\alpha = 2(c\alpha)
\quad\text{or}\quad
\alpha = -2(c\alpha),
\end{align*}
contradicting the same theorem with $\gamma=c\alpha$. Hence the only possibilities are $c=1$ and $c=-1$.
[/guided]
[/step]
[step:Assemble the abstract root system axioms]
We have shown that $E$ is a finite-dimensional real [inner product space](/page/Inner%20Product%20Space), that $\Phi \subset E$ is finite, that $0 \notin \Phi$, and that $\Phi$ spans $E$. For each $\alpha \in \Phi$, the reflection
\begin{align*}
s_\alpha(\beta)
= \beta-\frac{2(\beta,\alpha)}{(\alpha,\alpha)}\alpha
\end{align*}
preserves $\Phi$, and for every $\alpha,\beta \in \Phi$ the Cartan integer
\begin{align*}
\frac{2(\beta,\alpha)}{(\alpha,\alpha)}
\end{align*}
is an integer. Finally, if $c\alpha \in \Phi$ for $\alpha \in \Phi$ and $c \in \mathbb R$, then $c=\pm1$. These are precisely the axioms of a [reduced crystallographic root system](/page/Root%20System). Therefore $\Phi$ is a reduced crystallographic root system.
[/step]