[proofplan] We define a map $\varphi: \operatorname{Gal}(K/k) \to S_n$ by recording how each $k$-automorphism permutes the roots of $f$. The key observations are: (1) every $k$-automorphism must send roots of $f$ to roots of $f$, so the action is well-defined; (2) the action defines a group homomorphism by functoriality of composition; and (3) the homomorphism is injective because $K$ is generated over $k$ by the roots $\alpha_1, \ldots, \alpha_n$, so an automorphism fixing all roots is the identity. Divisibility of $|\operatorname{Gal}(K/k)|$ by $n!$ then follows from [Lagrange's Theorem](/theorems/782). [/proofplan]

[step:Verify that each $k$-automorphism permutes the roots of $f$]Let $\sigma \in \operatorname{Gal}(K/k)$. Since $f \in k[x]$ and $\sigma$ fixes $k$ pointwise, for each root $\alpha_i$ of $f$ we have \begin{align*} f(\sigma(\alpha_i)) = \sigma(f(\alpha_i)) = \sigma(0) = 0. \end{align*} Hence $\sigma(\alpha_i)$ is a root of $f$, so $\sigma(\alpha_i) \in \{\alpha_1, \ldots, \alpha_n\}$. Since $\sigma$ is injective (it is an automorphism) and $f$ is separable (the roots $\alpha_1, \ldots, \alpha_n$ are distinct), the map $\alpha_i \mapsto \sigma(\alpha_i)$ is an injection from the finite set $\{\alpha_1, \ldots, \alpha_n\}$ to itself, hence a bijection. Therefore $\sigma$ induces a permutation $\pi_\sigma \in S_n$ defined by $\sigma(\alpha_i) = \alpha_{\pi_\sigma(i)}$.[/step]

[guided]Why must a $k$-automorphism permute the roots? The polynomial $f$ has coefficients in $k$, and $\sigma$ fixes every element of $k$. So $\sigma$ fixes each coefficient of $f$, which means $f(\sigma(\alpha_i)) = \sigma(f(\alpha_i)) = \sigma(0) = 0$. This forces $\sigma(\alpha_i)$ to be a root of $f$. Why is the induced map on roots a bijection? We have $n$ roots (distinct because $f$ is separable) and $\sigma$ is injective (as a field automorphism). An injective map from a finite set to itself is automatically surjective, so $\sigma$ permutes the roots. We encode this permutation as an element $\pi_\sigma$ of the symmetric group $S_n$, where we use the labelling $\{\alpha_1, \ldots, \alpha_n\}$ to identify the root set with $\{1, \ldots, n\}$.[/guided]

[step:Define the homomorphism $\varphi: \operatorname{Gal}(K/k) \to S_n$ and verify the group homomorphism property] Define the map \begin{align*} \varphi: \operatorname{Gal}(K/k) &\to S_n \\ \sigma &\mapsto \pi_\sigma, \end{align*} where $\pi_\sigma$ is the permutation determined by $\sigma(\alpha_i) = \alpha_{\pi_\sigma(i)}$. We verify that $\varphi$ is a group homomorphism. For $\sigma, \tau \in \operatorname{Gal}(K/k)$ and each $1 \leq i \leq n$: \begin{align*} (\sigma \circ \tau)(\alpha_i) = \sigma(\tau(\alpha_i)) = \sigma(\alpha_{\pi_\tau(i)}) = \alpha_{\pi_\sigma(\pi_\tau(i))}. \end{align*} Hence $\pi_{\sigma \circ \tau}(i) = \pi_\sigma(\pi_\tau(i)) = (\pi_\sigma \circ \pi_\tau)(i)$ for all $i$, which gives $\varphi(\sigma \circ \tau) = \varphi(\sigma) \circ \varphi(\tau)$. [/step]

[step:Prove that $\varphi$ is injective]Suppose $\sigma \in \ker \varphi$, so that $\pi_\sigma = \operatorname{id}$, meaning $\sigma(\alpha_i) = \alpha_i$ for all $1 \leq i \leq n$. Since $K$ is the splitting field of $f$ over $k$, we have $K = k(\alpha_1, \ldots, \alpha_n)$. Every element of $K$ is a $k$-polynomial expression in $\alpha_1, \ldots, \alpha_n$, and $\sigma$ fixes each $\alpha_i$ and each element of $k$. Therefore $\sigma$ fixes every element of $K$, so $\sigma = \operatorname{id}_K$. Hence $\ker \varphi = \{\operatorname{id}_K\}$ and $\varphi$ is injective.[/step]

[guided]The kernel of $\varphi$ consists of those automorphisms that fix every root of $f$. But $K = k(\alpha_1, \ldots, \alpha_n)$ — the splitting field is generated over $k$ by the roots. Any $k$-automorphism that fixes all the generators and all of $k$ must fix every element of $K$ (since every element of $K$ is obtained from $k$ and the $\alpha_i$ by field operations, all of which are preserved by an automorphism). So $\ker \varphi = \{\operatorname{id}_K\}$. This is the crucial point where the hypothesis that $K$ is a **splitting field** is used. If $K$ were a larger extension containing the roots but also containing additional elements, an automorphism could fix all roots yet act non-trivially on those extra elements. But in a splitting field, the roots generate everything.[/guided]

[step:Conclude that $|\operatorname{Gal}(K/k)|$ divides $n!$] Since $\varphi: \operatorname{Gal}(K/k) \hookrightarrow S_n$ is an injective group homomorphism, the image $\varphi(\operatorname{Gal}(K/k))$ is a subgroup of $S_n$ isomorphic to $\operatorname{Gal}(K/k)$. By [Lagrange's Theorem](/theorems/782) applied to the finite group $S_n$ (which has order $|S_n| = n!$) and its subgroup $\varphi(\operatorname{Gal}(K/k))$, we obtain \begin{align*} |\operatorname{Gal}(K/k)| = |\varphi(\operatorname{Gal}(K/k))| \;\big|\; n!. \end{align*} [/step]