0PDI
Proof. Put and assume .
There are
, and
such that .
Lemma 8.2.4 shows that .
We have .
It follows from Lemma 8.2.4 that
.
Since ,
it follows that , hence .
Assume . We have for some
by Lemma 8.2.4.
Since , we have
. We deduce that ,
hence (Corollary 8.2.13).
So, .
Assume now , i.e., .
We have and (Corollary 8.2.13).
Assume . There is such that (Lemma 8.2.4).
Since , we have , hence also . As a consequence,
. We deduce that
.
We have and
, hence
and
. We have
.
Since and ,
it follows that , by
applying Lemma 8.2.4 to .
Since , we deduce that
,
hence (using Lemma 8.2.4 for
again).
Assume now . It follows that ,
hence .
There are
with .
Let for .
Consider minimal such that
.
Define
and
.
Let . Define
and to be the domain and codomain of , intersected
with .
Note that . Let and define by
|
|
|
Lemma 7.4.35 shows that and are braids and
. We
have and we deduce that
, where
.
We have . This completes the proof
of the first statement of the lemma.
The second statement of the lemma follows from the first one applied to
thanks to Remark 8.2.6.
∎