有限鏡映群

1：$P:=\bigcap_HU_H(C)$ は凸な開集合で連結であり、どの $H$ とも交わらず、$C\subset P$ である。$P$ は連結なので $C$ を含む連結成分 $C$ に含まれ、$C=P$ である。閉半空間の共通部分 $Q$ は閉集合で $P$ を含み、$y\in Q$、$c\in P$ なら $t\in(0,1]$ で $(1-t)y+tc\in P$ なので $y\in\overline{P}$、よって $\overline{P}=Q$ である。有限個の集合の共通部分の内部は内部の共通部分で、閉半空間の内部は開半空間なので、$\overline{C}$ の内部は $P=C$ である。
2：$w$ は $V$ の同相写像で $\bigcup_{H\in\mathcal{H}}H$ を自身に写すので、連結成分を連結成分に写す。$w\in\mathrm{O}(V)$ なので $(wx,w\alpha)=(x,\alpha)$ で、$w$ は $U_H(C)$ を $U_{wH}(wC)$ に写す。
3：$C$ と $D$ を隔てる $H$ がなければ、各 $H$ について $D\subset U_H(C)$ なので、1 により $D\subset C$、よって $D=C$ である。
4：各 $H$ は内部が空な閉集合で、有限個の和もそうである（$U$ が開集合で $U\subset A\cup B$、$A,B$ が内部が空な閉集合なら、$U\setminus A$ は $B$ に含まれる開集合で空、よって $U\subset A$、$U=\emptyset$）。したがって $x$ に収束する正則な点（どの $H$ にも属さない点）の列があり、部屋は有限個なので、ある部屋に無限個の項が入る。その部屋の閉包が $x$ を含む。$\square$

異なる $H,H'\in\mathcal{H}$ について $H\cap H'$ は $n-2$ 次元なので、$H\cap H'$ と $z$ で張られる部分空間 $L_{H,H'}$ は $V$ の真部分空間である。prf-frg-cone の 4 と同じ理由で、開集合 $C$ は有限個の $L_{H,H'}$ に覆われないので、どの $L_{H,H'}$ にも属さない $x\in C$ がとれる。
$x_t:=(1-t)x+tz$、$t_0:=\sup\{t\in[0,1]\mid x_s\in C\ (0\le s\le t)\}$、$p:=x_{t_0}$ とおく。$p\in\overline{C}$ で、$z\notin\overline{C}$ なので $t_0<1$、$C$ は開集合なので $p\notin C$ である。lem-frg-cone の 1 により、すべての $H$ で $(p,\alpha_H^C)\ge0$ で、ある $H$ で $(p,\alpha_H^C)=0$、すなわち $p\in H$ である。$p\in H\cap H'$（$H'\ne H$）なら $x=(p-t_0z)/(1-t_0)\in L_{H,H'}$ となり $x$ の選び方に反するので、$p$ を含む $\mathcal{H}$ の元は $H$ だけである。
$H$ が $C$ の壁であることを示す。$H'\ne H$ について $(p,\alpha_{H'}^C)>0$ なので、$p$ の近傍 $B$ でこれらがすべて正のものがある。$q\in B\cap H$ と小さい $\varepsilon>0$ について $q+\varepsilon\alpha_H^C$ はすべての $U_{H'}(C)$ に入り、lem-frg-cone の 1 により $C$ に属するので、$q\in\overline{C}$ である。よって $B\cap H\subset\overline{C}$ で、$H$ は壁である。$t\mapsto(x_t,\alpha_H^C)$ は 1 次関数で、$t=0$ で正、$t=t_0<1$ で $0$ なので、$t=1$ で負、すなわち $(z,\alpha_H^C)<0$ である。
後半：右辺を $P$ とすると $C\subset P$ で、$P$ は開集合である。$y\in P\setminus C$ があれば、$\overline{C}$ の内部は $C$ なので（lem-frg-cone の 1）、$y$ の近傍で $P$ に含まれるものは $\overline{C}$ に含まれず、$P\setminus\overline{C}$ の点 $z$ がある。前半の壁 $H$ について $z\notin U_H(C)\supset P$ となり矛盾する。$\square$

$H\cap\overline{C}$ が含む $H$ の空でない開集合は、有限個の $H\cap H'$（$H'\ne H$、$H$ の真部分空間）では覆われないので、どの $H'\ne H$ にも属さない点 $p\in H\cap\overline{C}$ がある。$p$ を中心とする開球 $B$ で、$H'\ne H$ と交わらないものをとる。$B^{+}:=B\cap U_H(C)$ はすべての $U_{H'}(C)$ に含まれる（$p\in\overline{C}\setminus H'$ で $B$ は $H'$ の片側にある）ので $C$ に含まれる。$s$ は $p$ を固定する等長変換なので $s(B)=B$ で、$(sx,\alpha_H^C)=-(x,\alpha_H^C)$ から $s(B^{+})=B^{-}:=B\cap\{(x,\alpha_H^C)<0\}$ である。よって $B^{-}\subset sC$ である。$H'\ne H$ について $B^{+}$ と $B^{-}$ は $H'$ の同じ側にあるので $H'$ は $C$ と $sC$ を隔てず、$H$ は隔てる。$\square$

$W_0:=\langle S\rangle$ とおく。
推移性：部屋 $D$ と $y\in D$、$x\in C$ をとる。$W_0$ は有限なので、$\lvert wy-x\rvert$ を最小にする $w\in W_0$ がある。$wy$ はどの $H\in\mathcal{H}$ にも属さない（$W$ は $\mathcal{H}$ を置換する）。$wy\notin C$ と仮定すると、$wy$ は別の部屋にあり、$\overline{C}\setminus C$ は $\bigcup H$ に含まれるので $wy\notin\overline{C}$ である。lem-frg-walls により $C$ の壁 $H$ で $\beta:=(wy,\alpha)<0$（$\alpha=\alpha_H^C$）となるものがある。$s=s_H\in S$ について $swy=wy-2\beta\alpha$ だから
$$ \lvert swy-x\rvert^2=\lvert wy-x\rvert^2-4\beta(wy-x,\alpha)+4\beta^2=\lvert wy-x\rvert^2+4\beta(x,\alpha)< \lvert wy-x\rvert^2 $$
で、$sw\in W_0$ は最小性に反する。よって $wy\in C$、$wD=C$ である。
生成：$H\in\mathcal{H}$ をとる。$H$ の点 $p$ でほかの $H'\in\mathcal{H}$ に属さないものをとり、$p$ のまわりの開球 $B$ で $H'\neq H$ と交わらないものをとる。$B\setminus H$ の 2 つの半球の一方を含む部屋 $D$ について、$B\cap H\subset\overline{D}$ なので $H$ は $D$ の壁である。推移性により $wD=C$（$w\in W_0$）となり、$w$ は線形な同相写像で $H\cap\overline{D}$ を $wH\cap\overline{C}$ に、$H$ の開集合を $wH$ の開集合に写すので $wH$ は $C$ の壁、$s_{wH}\in S$ である。$s_H=w^{-1}s_{wH}w\in W_0$ である。$W$ は鏡映 $s_H$（$H\in\mathcal{H}$）で生成されるので $W=W_0$ であり、1 が示された。
ギャラリー：$s_1,\dots,s_k\in S$、$u_i:=s_1\cdots s_i$（$u_0=1$）、$C_i:=u_iC$ とする。$C_{i-1}=u_{i-1}C$ と $C_i=u_{i-1}s_iC$ を隔てる $\mathcal{H}$ の元は、lem-frg-adjacent を $u_{i-1}$ で写して（lem-frg-cone の 2）、$H_i:=u_{i-1}H_{s_i}$ だけである。したがって $H\in\mathcal{H}$ について、$C_0$ と $C_k$ が $H$ に隔てられることは、$H_i=H$ となる $i$ の個数が奇数であることと同値である。とくに $d(C,u_kC)\le k$ で、$d(C,wC)\le\ell(w)$ である。
2 文字の消去：$H_i=H_j$（$i< j$）とする。$H_i$ の鏡映は $u_{i-1}s_iu_{i-1}^{-1}=u_{j-1}s_ju_{j-1}^{-1}$ である。$u_{j-1}^{-1}u_{i-1}=s_{j-1}\cdots s_i$ なので $s_j=(s_{j-1}\cdots s_{i+1}s_i)\,s_i\,(s_i s_{i+1}\cdots s_{j-1})=s_{j-1}\cdots s_{i+1}s_is_{i+1}\cdots s_{j-1}$ となり、左から $s_i\cdots s_{j-1}$ を掛けて
$$ s_is_{i+1}\cdots s_j=s_{i+1}\cdots s_{j-1},\qquad\text{よって}\qquad s_1\cdots s_k=s_1\cdots\widehat{s_i}\cdots\widehat{s_j}\cdots s_k $$
である。
2 と 5：$w=s_1\cdots s_k$ が簡約表示なら、上の消去で長さ $k-2$ の表示ができてしまうので $H_1,\dots,H_k$ は相異なる。各 $H_i$ はちょうど 1 回またがれるので $C$ と $wC$ を隔て、隔てる超平面はどれかの $H_i$ なので $d(C,wC)=k=\ell(w)$ である。表示 $s_1\cdots s_k$ が簡約でない（$k>\ell(w)=d(C,wC)$）なら、$H_i$ が相異なると $d(C,wC)=k$ となって矛盾するので、$H_i=H_j$（$i< j$）があり、2 文字を消せる。これが消去条件である。$S$ の元は位数 $2$ で $W$ を生成するので、Coxeter系 の系「Coxeter系の同値な特徴づけ」により $(W,S)$ は Coxeter 系である。ただし、消去条件から Coxeter 系が従うこと（同記事の定理「消去条件からCoxeter系へ」）はこの記事では証明しない（Dav07 Theorem 6.6.3 (i) も参照）。
3：$wC=C$ なら 2 により $\ell(w)=d(C,C)=0$、$w=1$ である。
4：$x\in V$ はある部屋 $D$ の閉包に属し（lem-frg-cone の 4）、$wD=C$ となる $w$ について $wx\in\overline{C}$ である。後半を $\ell(w)$ についての帰納法で示す。$\ell(w)=0$ なら明らかである。$w=s_1\cdots s_k$（$k\ge1$）を簡約表示とすると、2 の証明により $H_1=H_{s_1}$ は $C$ と $wC$ を隔てる。$\alpha:=\alpha_{H_1}^C$ とすると、$y\in\overline{C}$ から $(y,\alpha)\ge0$、$y=wx\in\overline{wC}$ から $(y,\alpha)\le0$ なので、$y\in H_1$、$s_1y=y$ である。$s_1w=s_2\cdots s_k$ は長さ $k-1$ で $(s_1w)x=y$ なので、帰納法の仮定から $x=y$、$s_1w\in\langle S_x\rangle$ である。$s_1\in S_y=S_x$ なので $w\in\langle S_x\rangle$ である。$\square$

1：$wv\in\overline{C}$ となる $w$ をとると、$W_v=w^{-1}W_{wv}w$ で、$W_{wv}$ は $S_{wv}$ で生成されるので、$W_v$ は $w^{-1}sw=s_{w^{-1}H_s}$（$s\in S_{wv}$）で生成される。$w^{-1}H_s$ は $v$ を含むので、これらは $v$ を固定する鏡映である。
2：$-1$ は $\bigcup H$ を保つ同相写像なので $-C$ は部屋で、主定理の 3 により $w_0$ がただ 1 つある。すべての $H$ について $-C\subset\{(x,\alpha_H^C)<0\}$ なので、どの $H$ も $C$ と $-C$ を隔て、$\ell(w_0)=d(C,-C)=\lvert\mathcal{H}\rvert$ である。$H\mapsto s_H$ は $\mathcal{H}$ と $W$ の鏡映の全体の全単射である。$\ell(w)=d(C,wC)\le\lvert\mathcal{H}\rvert$ である。$\square$