An element with full left descent makes the Coxeter group finite and is the longest element

Assume $D_L(x)=S$. Then $\rho (x^{-1}){\mathrm{\Phi }}_{+}={\mathrm{\Phi }}_{-}$: for every $s\in S$ the hypothesis and [F4] give $\rho (x^{-1})e_s\in {\mathrm{\Phi }}_{-}$. Every $\alpha \in {\mathrm{\Phi }}_{+}$ has the form $\alpha ={\sum }_s{\lambda }_s{e}_s$ with all ${\lambda }_s\ge 0$ by [F3], so by linearity of $\rho (x^{-1})$ the image $\rho (x^{-1})\alpha ={\sum }_s{\lambda }_s\rho (x^{-1})e_s$ is a nonnegative combination of elements of ${\mathrm{\Phi }}_{-}\subseteq -V_{+}$, hence lies in $-V_{+}$, and it is nonzero because $\rho (x^{-1})$ is injective and $\alpha \mathrm{\ne }0$; thus $\rho (x^{-1})\alpha \in \mathrm{\Phi }\cap (-V_{+}\setminus \{0\})={\mathrm{\Phi }}_{-}$, giving $\rho (x^{-1}){\mathrm{\Phi }}_{+}\subseteq {\mathrm{\Phi }}_{-}$. Replacing $\alpha$ by $-\alpha$ shows $\rho (x^{-1}){\mathrm{\Phi }}_{-}\subseteq {\mathrm{\Phi }}_{+}$, using ${\mathrm{\Phi }}_{-}=-{\mathrm{\Phi }}_{+}$ and linearity; since $\rho (x^{-1})$ permutes $\mathrm{\Phi }$ by [F2], these two inclusions force $\rho (x^{-1}){\mathrm{\Phi }}_{+}={\mathrm{\Phi }}_{-}$.

Under the hypothesis of step 1.1, $N(x^{-1})={\mathrm{\Phi }}_{+}$: by definition $N(x^{-1})=\{\alpha \in {\mathrm{\Phi }}_{+}:\rho (x^{-1})\alpha \in {\mathrm{\Phi }}_{-}\}$, and step 1.1 maps all of ${\mathrm{\Phi }}_{+}$ into ${\mathrm{\Phi }}_{-}$.

Under the hypothesis of step 1.1, $\mathrm{\Phi }$ is finite and $\mathrm{\mid }{\mathrm{\Phi }}_{+}\mathrm{\mid }=\mathrm{\ell }(x)=\mathrm{\mid }T\mathrm{\mid }$, and $W$ is finite. By [F15], $\mathrm{\ell }(x^{-1})=\mathrm{\ell }(x)$, and [F6] gives $\mathrm{\mid }N(x^{-1})\mathrm{\mid }=\mathrm{\ell }(x^{-1})$, so step 2.1 gives $\mathrm{\mid }{\mathrm{\Phi }}_{+}\mathrm{\mid }=\mathrm{\ell }(x)$; as $\mathrm{\Phi }={\mathrm{\Phi }}_{+}\bigsqcup {\mathrm{\Phi }}_{-}$ with ${\mathrm{\Phi }}_{-}=-{\mathrm{\Phi }}_{+}$, the root system $\mathrm{\Phi }$ is finite, the map ${\mathrm{\Phi }}_{+}\to T$ is a bijection, and $\rho$ embeds $W$ into the finite symmetric group $\mathrm{S}\mathrm{y}\mathrm{m}(\mathrm{\Phi })$, so $W$ is finite.

Under the hypothesis of step 1.1, $x$ is the longest element $w_0$ of $W$, and $x^{-1}=x$ and $\mathrm{\ell }(w_{0}w)=\mathrm{\ell }(w_0)-\mathrm{\ell }(w)$ for all $w$. Since $W$ is finite by step 3.1, [F11] gives a unique $w_0$ with $N(w_0^{-1})={\mathrm{\Phi }}_{+}$; step 2.1 says $N(x^{-1})={\mathrm{\Phi }}_{+}$, so $x=w_0$; the remaining properties are the listed clauses of [F11] (1).

Now let $J\subseteq S$ and let $w\in W_J$ satisfy $\mathrm{\ell }(sw)<\mathrm{\ell }(w)$ for every $s\in J$; then $W_J$ is finite, $N_J(w^{-1})={\mathrm{\Phi }}_J^{+}$ and $w=w_0(J)$. For each $s\in J$, [F4] turns the hypothesis into $\rho (w^{-1})e_s\in {\mathrm{\Phi }}_{-}$; since $\rho (w^{-1})$ preserves $V_J$ by [F9] and $e_s\in V_J$, this image lies in $\mathrm{\Phi }\cap V_J\cap {\mathrm{\Phi }}_{-}={\mathrm{\Phi }}_J^{-}$, so $\rho (w^{-1})e_s\in {\mathrm{\Phi }}_J^{-}$ for every $s\in J$. Every $\alpha \in {\mathrm{\Phi }}_J^{+}$ is a nonnegative combination of the $e_s$ by [F3]; because $\alpha \in V_J$ and the $e_s$ form a basis by [F1], its coordinates outside $J$ are zero, so it is a nonnegative combination ${\sum }_{s\in J}{\lambda }_s{e}_s$. Thus the computation of step 1.1, carried out inside the invariant subspace $V_J$ and using that $\rho (w^{-1})$ permutes ${\mathrm{\Phi }}_J$ (it sends $\rho (u)e_s$ to $\rho (w^{-1}u)e_s$ with $w^{-1}u\in W_J$), yields $\rho (w^{-1}){\mathrm{\Phi }}_J^{+}={\mathrm{\Phi }}_J^{-}$, that is $N_J(w^{-1})={\mathrm{\Phi }}_J^{+}$. The pair $(W_J,J)$ is a Coxeter system whose intrinsic length is the restriction of $\mathrm{\ell }$ by [F10]. For $s\in J$ and $v\in V_J$, [F2], [F12] and [F13] give $\rho (s)v=r_{e_s}(v)=v-2B(v,e_s)e_s$; this lies in $V_J$ and is the simple reflection for the restricted Coxeter form. Since [F9] makes $V_J$ invariant under every $\rho (u)$ with $u\in W_J$, the restriction $\rho {\mathrm{\mid }}_{W_J}$ is a homomorphism to $\mathrm{G}\mathrm{L}(V_J)$. It agrees on generators with the canonical reflection representation of $(W_J,J)$; uniqueness from the presented-group universal property [F14] makes the two representations equal, and their root system is exactly ${\mathrm{\Phi }}_J$ by the definition in the statement. Applying [F6] inside this subsystem gives $\mathrm{\mid }{\mathrm{\Phi }}_J^{+}\mathrm{\mid }=\mathrm{\mid }{N}_J(w^{-1})\mathrm{\mid }={\mathrm{\ell }}_J(w^{-1})=\mathrm{\ell }(w^{-1})=\mathrm{\ell }(w)$, using [F10] for intrinsic length and [F15] for inversion invariance. Since ${\mathrm{\Phi }}_J={\mathrm{\Phi }}_J^{+}\bigsqcup (-{\mathrm{\Phi }}_J^{+})$, the subsystem root set is finite. Its canonical representation is faithful by [F7] applied to the restricted matrix, so $W_J$ embeds in $\mathrm{S}\mathrm{y}\mathrm{m}({\mathrm{\Phi }}_J)$ and is finite. Since $W_J$ is finite, clause (1) of this lemma, whose proof consists of steps 1.1, 2.1, 3.1 and 4.1 and applies to any finite Coxeter system, gives on the subsystem a unique element $w_0(J)$ with $N_J(w_0(J{)}^{-1})={\mathrm{\Phi }}_J^{+}$; since $w$ has this property, $w=w_0(J)$, the longest element of $(W_J,J)$. No Choice was used anywhere in this proof.