[proofplan] The proof proceeds in three parts. For Part 1 (the bijective correspondence), we show that $\Psi \circ \Phi = \operatorname{id}$ and $\Phi \circ \Psi = \operatorname{id}$. The first identity uses [Artin's Lemma](/theorems/1272): given a subgroup $H \le G$, Artin's Lemma gives $[L : L^H] = |H|$, which forces $\operatorname{Gal}(L/L^H) = H$ by a cardinality squeeze. The second identity uses the fact that $L/F$ is Galois for every intermediate field $F$ (by [Normality Over Intermediate Fields](/theorems/1270)), reducing to the same Artin argument applied to the extension $L/F$. The degree formula $[G : H] = [L^H : K]$ then follows from the [Tower Law](/theorems/1248). For Part 2 (normal sub-extensions), we establish the conjugation identity $L^{\phi H \phi^{-1}} = \phi(L^H)$, which reduces the normality of $H$ in $G$ to the invariance of $L^H$ under all elements of $G$. We then show this invariance is equivalent to $L^H/K$ being a normal extension, using the characterisation of normality via splitting of minimal polynomials and the fact that $K$-automorphisms of $L$ permute roots of irreducible polynomials over $K$. For Part 3 (quotient groups), the restriction homomorphism $\rho: G \to \operatorname{Gal}(L^H/K)$ is well-defined by Part 2, has kernel $H$ by Part 1, and is surjective by comparing cardinalities using the degree formula from Part 1 and the Galois degree identity for $L^H/K$. [/proofplan]

[step:Show $\Psi \circ \Phi = \operatorname{id}$: every subgroup $H \le G$ satisfies $\operatorname{Gal}(L/L^H) = H$]Let $H$ be a subgroup of $G = \operatorname{Gal}(L/K)$. Every element of $H$ fixes $L^H := \{a \in L : \sigma(a) = a \text{ for all } \sigma \in H\}$ pointwise, so $H \subset \operatorname{Gal}(L/L^H)$. We apply [Artin's Lemma](/theorems/1272) to the finite group $H$ acting as automorphisms of $L$. The hypotheses are satisfied: $H$ is a finite group (as a subgroup of the finite group $G$) and every element of $H$ is a field automorphism of $L$ (since $G \subset \operatorname{Aut}(L)$). Artin's Lemma gives $[L : L^H] = |H|$. Since $[L : L^H]$ is finite, the [Bound on Automorphisms](/theorems/1255) gives $|\operatorname{Gal}(L/L^H)| \le [L : L^H] = |H|$. Combined with $H \subset \operatorname{Gal}(L/L^H)$, we obtain $|H| \le |\operatorname{Gal}(L/L^H)| \le |H|$, forcing $\operatorname{Gal}(L/L^H) = H$.[/step]

[guided]The goal is to show that the fixed-field map $\Phi: H \mapsto L^H$ is injective in the sense that distinct subgroups yield distinct fixed fields, and moreover the Galois group of $L$ over $L^H$ recovers $H$ exactly. The strategy is a cardinality squeeze: we establish both $H \subset \operatorname{Gal}(L/L^H)$ and $|\operatorname{Gal}(L/L^H)| \le |H|$, which together force equality. **The easy inclusion.** By definition, $L^H = \{a \in L : \sigma(a) = a \text{ for all } \sigma \in H\}$. If $\sigma \in H$, then $\sigma$ fixes every element of $L^H$, so $\sigma \in \operatorname{Gal}(L/L^H)$. This gives $H \subset \operatorname{Gal}(L/L^H)$, hence $|H| \le |\operatorname{Gal}(L/L^H)|$. **The reverse bound via Artin's Lemma.** We apply [Artin's Lemma](/theorems/1272). This theorem requires a finite group of automorphisms of a field. We verify the hypotheses: - $H$ is a subgroup of $G = \operatorname{Gal}(L/K)$, and $|G| = [L : K] < \infty$ by the hypothesis that $L/K$ is a finite Galois extension, so $H$ is finite. - Each element of $H$ is an element of $G \subset \operatorname{Aut}(L)$, hence a field automorphism of $L$. Artin's Lemma concludes that $[L : L^H] = |H|$. Now, every element of $\operatorname{Gal}(L/L^H)$ is an $L^H$-automorphism of $L$. Any such automorphism permutes the roots of each irreducible polynomial over $L^H$ that has a root in $L$. Since $[L : L^H] = |H| < \infty$, the [Bound on Automorphisms](/theorems/1255) gives $|\operatorname{Gal}(L/L^H)| \le [L : L^H] = |H|$. Combining the two inequalities: $|H| \le |\operatorname{Gal}(L/L^H)| \le |H|$. Since $H \subset \operatorname{Gal}(L/L^H)$ and both are finite sets of the same cardinality, $\operatorname{Gal}(L/L^H) = H$. This is the heart of the Galois correspondence: Artin's Lemma provides the precise degree bound that prevents the Galois group from being larger than $H$.[/guided]

[step:Show $\Phi \circ \Psi = \operatorname{id}$: every intermediate field $F$ satisfies $L^{\operatorname{Gal}(L/F)} = F$]Let $F$ be an intermediate field with $K \subset F \subset L$. By [Normality Over Intermediate Fields](/theorems/1270), the extension $L/F$ is Galois. (The hypotheses of that theorem are satisfied: $L/K$ is a finite Galois extension and $F$ is an intermediate field.) In particular, $|\operatorname{Gal}(L/F)| = [L : F]$. Set $H := \operatorname{Gal}(L/F)$. Every element of $F$ is fixed by every element of $H$, so $F \subset L^H$. By [Artin's Lemma](/theorems/1272) applied to the finite group $H$ of automorphisms of $L$, $[L : L^H] = |H| = [L : F]$. Since $F \subset L^H \subset L$, the [Tower Law](/theorems/1248) gives \begin{align*} [L : F] = [L : L^H] \cdot [L^H : F] = [L : F] \cdot [L^H : F], \end{align*} which forces $[L^H : F] = 1$, i.e., $L^H = F$.[/step]

[guided]The question is whether $\operatorname{Gal}(L/F)$ retains enough information to reconstruct $F$ as a fixed field. The key ingredient is that $L/F$ is itself a Galois extension — this is not automatic and requires verification. **Why $L/F$ is Galois.** We apply [Normality Over Intermediate Fields](/theorems/1270), which states: if $L/K$ is a finite Galois extension and $K \subset F \subset L$, then $L/F$ is also Galois. We verify the hypotheses: - $L/K$ is a finite Galois extension by the theorem's hypothesis. - $K \subset F \subset L$ is an intermediate field by assumption. The theorem's conclusion gives us $L/F$ is Galois, so $|\operatorname{Gal}(L/F)| = [L : F]$. To see why this matters: without knowing that $L/F$ is Galois, we would only have $|\operatorname{Gal}(L/F)| \le [L : F]$, and the degree comparison below would not produce equality. **The degree comparison.** Set $H := \operatorname{Gal}(L/F)$. Since every automorphism in $H$ fixes $F$ pointwise, we have $F \subset L^H$. We need $L^H = F$, i.e., the fixed field is not larger than $F$. By [Artin's Lemma](/theorems/1272), applied to the finite group $H \subset \operatorname{Aut}(L)$ (which is valid since $|H| = [L:F] < \infty$), we obtain $[L : L^H] = |H| = [L : F]$. Now $F \subset L^H \subset L$, so the [Tower Law](/theorems/1248) gives \begin{align*} [L : F] = [L : L^H] \cdot [L^H : F]. \end{align*} Substituting $[L : L^H] = [L : F]$: \begin{align*} [L : F] = [L : F] \cdot [L^H : F]. \end{align*} Since $[L : F] \ge 1$ (and finite), dividing gives $[L^H : F] = 1$, so $L^H = F$. This confirms that $\Phi \circ \Psi$ is the identity on intermediate fields: starting from $F$, forming $\operatorname{Gal}(L/F)$, and taking the fixed field returns us to $F$.[/guided]

[step:Derive the degree-index formula $[G : H]= [L^H : K]$ and the inclusion-reversal property] Let $H \le G$. By [Artin's Lemma](/theorems/1272), $[L : L^H] = |H|$. Since $L/K$ is Galois, $|G| = [L : K]$. The [Tower Law](/theorems/1248) applied to $K \subset L^H \subset L$ gives \begin{align*} [L : K] &= [L : L^H] \cdot [L^H : K], \\ |G| &= |H| \cdot [L^H : K]. \end{align*} Dividing, $[L^H : K] = |G| / |H| = [G : H]$. For the inclusion-reversal: if $H_1 \le H_2 \le G$, then every element of $H_1$ fixes $L^{H_1}$ and every element of $H_2 \supset H_1$ fixes $L^{H_2}$. Since $H_1 \subset H_2$, every automorphism fixing $L^{H_2}$ also fixes $L^{H_2}$, but the elements of $H_2 \setminus H_1$ need not fix all of $L^{H_1}$. Precisely: $L^{H_2} = \{a \in L : \sigma(a) = a \text{ for all } \sigma \in H_2\} \subset \{a \in L : \sigma(a) = a \text{ for all } \sigma \in H_1\} = L^{H_1}$, so $H_1 \le H_2$ implies $L^{H_1} \supset L^{H_2}$. The converse follows from the bijection: if $L^{H_1} \supset L^{H_2}$, then $H_1 = \operatorname{Gal}(L/L^{H_1}) \le \operatorname{Gal}(L/L^{H_2}) = H_2$. This completes Part 1.[/step]

[guided]The degree-index formula connects the group-theoretic index $[G:H]$ to the field-theoretic degree $[L^H : K]$, making the Galois correspondence a quantitative bijection. By hypothesis, $L/K$ is Galois with $|G| = |\operatorname{Gal}(L/K)| = [L : K]$. For a subgroup $H \le G$, [Artin's Lemma](/theorems/1272) gives $[L : L^H] = |H|$. The tower of extensions $K \subset L^H \subset L$ satisfies the [Tower Law](/theorems/1248): \begin{align*} [L : K] = [L : L^H] \cdot [L^H : K]. \end{align*} Substituting $[L : K] = |G|$ and $[L : L^H] = |H|$: \begin{align*} |G| = |H| \cdot [L^H : K], \end{align*} so $[L^H : K] = |G|/|H| = [G : H]$. This formula makes the order-reversal precise: a larger subgroup $H$ (larger $|H|$, hence smaller $[G:H]$) corresponds to a smaller intermediate field $L^H$ (smaller $[L^H : K]$). The extreme cases confirm this: - $H = G$ gives $[L^G : K] = [G : G] = 1$, so $L^G = K$: the full Galois group fixes only the base field. - $H = \{e\}$ gives $[L^{\{e\}} : K] = [G : \{e\}] = |G| = [L : K]$, so $L^{\{e\}} = L$: the trivial subgroup fixes everything. **The inclusion-reversal property.** For $H_1 \le H_2 \le G$: if $a \in L^{H_2}$, then $\sigma(a) = a$ for all $\sigma \in H_2$, hence for all $\sigma \in H_1 \subset H_2$, so $a \in L^{H_1}$. This gives $L^{H_2} \subset L^{H_1}$. Conversely, if $L^{H_1} \supset L^{H_2}$, then every automorphism fixing $L^{H_1}$ pointwise also fixes the smaller field $L^{H_2}$ pointwise, so $\operatorname{Gal}(L/L^{H_1}) \le \operatorname{Gal}(L/L^{H_2})$. Since $\Psi \circ \Phi = \operatorname{id}$ (from the first step), $\operatorname{Gal}(L/L^{H_i}) = H_i$, giving $H_1 \le H_2$.[/guided]

[step:Establish the conjugation identity $L^{\phi H \phi^{-1}} = \phi(L^H)$ for all $\phi \in G$]Let $H \le G$ and $\phi \in G$. For $a \in L$: \begin{align*} a \in L^{\phi H \phi^{-1}} &\iff (\phi h \phi^{-1})(a) = a \quad \text{for all } h \in H \\ &\iff \phi(h(\phi^{-1}(a))) = a \quad \text{for all } h \in H \\ &\iff h(\phi^{-1}(a)) = \phi^{-1}(a) \quad \text{for all } h \in H \\ &\iff \phi^{-1}(a) \in L^H \\ &\iff a \in \phi(L^H). \end{align*} The third equivalence uses injectivity of $\phi$: since $\phi$ is a field automorphism, $\phi(b) = a$ has the unique solution $b = \phi^{-1}(a)$, so $\phi(h(\phi^{-1}(a))) = a$ holds if and only if $h(\phi^{-1}(a)) = \phi^{-1}(a)$.[/step]

[guided]This identity is the algebraic mechanism underlying Part 2. It translates the group-theoretic operation of conjugation ($H \mapsto \phi H \phi^{-1}$) into the field-theoretic operation of applying an automorphism to the fixed field ($L^H \mapsto \phi(L^H)$). We verify the identity element-by-element. Fix $a \in L$ and unwind the definitions: \begin{align*} a \in L^{\phi H \phi^{-1}} &\iff (\phi h \phi^{-1})(a) = a \quad \text{for all } h \in H \\ &\iff \phi(h(\phi^{-1}(a))) = a \quad \text{for all } h \in H \\ &\iff h(\phi^{-1}(a)) = \phi^{-1}(a) \quad \text{for all } h \in H \\ &\iff \phi^{-1}(a) \in L^H \\ &\iff a \in \phi(L^H). \end{align*} The crucial step is the third equivalence. Why can we "cancel" $\phi$ from both sides? Because $\phi$ is a field automorphism, hence injective: $\phi(x) = \phi(y)$ implies $x = y$. So $\phi(h(\phi^{-1}(a))) = a = \phi(\phi^{-1}(a))$ is equivalent to $h(\phi^{-1}(a)) = \phi^{-1}(a)$. Why does this identity matter for Part 2? There are two key consequences: - If $H \trianglelefteq G$, then $\phi H \phi^{-1} = H$ for every $\phi \in G$, so $\phi(L^H) = L^{\phi H \phi^{-1}} = L^H$. That is, the fixed field $L^H$ is invariant under every element of $G$. - Conversely, if $\phi(L^H) = L^H$ for every $\phi \in G$, then $L^{\phi H \phi^{-1}} = L^H$ for every $\phi \in G$. Since $\Phi$ is a bijection (Part 1), equal fixed fields imply equal subgroups: $\phi H \phi^{-1} = H$ for all $\phi$, i.e., $H \trianglelefteq G$. This reduces Part 2 to characterising when the fixed field $L^H$ is invariant under all of $G$ in terms of the extension $L^H/K$.[/guided]

[step:Prove the normality criterion: $H \trianglelefteq G$ if and only if $L^H/K$ is a normal extension]By the conjugation identity, $H \trianglelefteq G$ if and only if $\phi(L^H) = L^H$ for all $\phi \in G$. We show this condition is equivalent to $L^H/K$ being normal. **Forward direction ($H \trianglelefteq G$ implies $L^H/K$ normal).** Assume $\phi(L^H) = L^H$ for all $\phi \in G$. Let $\alpha \in L^H$ and let $p := \operatorname{min}_K(\alpha) \in K[t]$. Since $L/K$ is normal, all roots of $p$ lie in $L$. Let $\beta$ be any root of $p$ in $L$. Since $p$ is irreducible over $K$ and both $\alpha, \beta$ are roots of $p$, there exists a $K$-isomorphism $K(\alpha) \to K(\beta)$ sending $\alpha \mapsto \beta$. Since $L/K$ is normal, this $K$-embedding of $K(\alpha)$ into $L$ extends to a $K$-automorphism $\phi \in G$ of $L$. (This extension property characterises normal extensions: every $K$-embedding of a subextension into $\overline{K}$ maps into $L$ itself, hence yields an element of $\operatorname{Aut}_K(L) = G$.) Since $\alpha \in L^H$ and $\phi(L^H) = L^H$, we have $\beta = \phi(\alpha) \in L^H$. Since $\beta$ was an arbitrary root of $p$ in $L$, all roots of $\operatorname{min}_K(\alpha)$ lie in $L^H$. Since $\alpha \in L^H$ was arbitrary, $L^H/K$ is a normal extension. Moreover, $L^H/K$ is separable: every element of $L^H \subset L$ is separable over $K$ because $L/K$ is separable. Hence $L^H/K$ is both normal and separable, i.e., Galois. **Backward direction ($L^H/K$ normal implies $H \trianglelefteq G$).** Assume $L^H/K$ is a normal extension. Let $\phi \in G$ and $\alpha \in L^H$. Since $\phi$ is a $K$-automorphism of $L$, $\phi(\alpha)$ is a root of $\operatorname{min}_K(\alpha)$ in $L$. By normality of $L^H/K$, all roots of $\operatorname{min}_K(\alpha)$ that lie in $L$ already lie in $L^H$, so $\phi(\alpha) \in L^H$. Since $\alpha \in L^H$ was arbitrary, $\phi(L^H) \subset L^H$. Since $\phi|_{L^H}: L^H \to L^H$ is an injective $K$-algebra homomorphism (as a restriction of a field automorphism) and $L^H$ is a finite-dimensional $K$-vector space (with $[L^H : K] = [G : H] < \infty$), an injective linear map between finite-dimensional vector spaces of the same dimension is surjective. Hence $\phi(L^H) = L^H$. Since $\phi(L^H) = L^H$ holds for every $\phi \in G$, the conjugation identity gives $L^{\phi H \phi^{-1}} = \phi(L^H) = L^H$ for all $\phi \in G$. Since $\Phi$ is injective (Part 1), $\phi H \phi^{-1} = H$ for all $\phi \in G$, i.e., $H \trianglelefteq G$. This completes Part 2: $H \trianglelefteq G$ if and only if $L^H/K$ is normal, which (since $L/K$ is separable) holds if and only if $L^H/K$ is Galois.[/step]

[guided]We assume $H \trianglelefteq G$ and must show that $L^H/K$ is a normal extension. Recall that $L^H/K$ is normal if and only if, for every $\alpha \in L^H$, the minimal polynomial $\operatorname{min}_K(\alpha)$ splits completely over $L^H$. Fix $\alpha \in L^H$ and let $p := \operatorname{min}_K(\alpha) \in K[t]$. Since $L/K$ is normal, all roots of $p$ lie in $L$. The task is to show they all lie in the subfield $L^H$. Let $\beta \in L$ be any root of $p$. Since $\alpha$ and $\beta$ are roots of the same irreducible polynomial $p \in K[t]$, the map $\alpha \mapsto \beta$ defines a $K$-isomorphism $K(\alpha) \to K(\beta)$. We now use the extension property of normal extensions: since $L/K$ is normal, every $K$-embedding of a subextension of $L$ into an algebraic closure $\overline{K} \supset L$ has image contained in $L$. In particular, the $K$-embedding $K(\alpha) \hookrightarrow L$ sending $\alpha \mapsto \beta$ extends to a $K$-automorphism $\phi: L \to L$, so $\phi \in G = \operatorname{Gal}(L/K)$ and $\phi(\alpha) = \beta$. Now we use the hypothesis $H \trianglelefteq G$. The conjugation identity gives $\phi(L^H) = L^{\phi H \phi^{-1}} = L^H$ (since $\phi H \phi^{-1} = H$). Therefore $\beta = \phi(\alpha) \in \phi(L^H) = L^H$. Since $\beta$ was an arbitrary root of $p$ in $L$, all roots of $\operatorname{min}_K(\alpha)$ lie in $L^H$. Since $\alpha \in L^H$ was arbitrary, every minimal polynomial over $K$ of an element of $L^H$ splits completely in $L^H$. This is precisely the definition of $L^H/K$ being normal. Finally, $L^H/K$ is also separable: for any $\alpha \in L^H$, the minimal polynomial $\operatorname{min}_K(\alpha)$ divides $\operatorname{min}_K(\alpha)$ computed in the larger extension $L/K$, and $L/K$ is separable, so $\operatorname{min}_K(\alpha)$ has no repeated roots. (More directly: $\alpha \in L^H \subset L$ and $L/K$ is separable, so $\alpha$ is separable over $K$.) Hence $L^H/K$ is both normal and separable, i.e., Galois.[/guided]

[step:Construct the quotient isomorphism $G/H \xrightarrow{\sim} \operatorname{Gal}(L^H/K)$ via restriction]Assume $H \trianglelefteq G$. By Part 2, $L^H/K$ is Galois and $\phi(L^H) = L^H$ for all $\phi \in G$. Define the restriction homomorphism \begin{align*} \rho: G &\to \operatorname{Gal}(L^H/K) \\ \phi &\mapsto \phi|_{L^H}. \end{align*} **Well-definedness.** For $\phi \in G$: since $\phi(L^H) = L^H$ (from Part 2) and $\phi$ fixes $K$ pointwise (since $\phi \in G = \operatorname{Gal}(L/K)$), the restriction $\phi|_{L^H}$ is a $K$-automorphism of $L^H$, i.e., an element of $\operatorname{Gal}(L^H/K)$. **Homomorphism property.** For $\phi, \psi \in G$ and $\alpha \in L^H$: \begin{align*} \rho(\phi \circ \psi)(\alpha) = (\phi \circ \psi)(\alpha) = \phi(\psi(\alpha)) = \rho(\phi)(\rho(\psi)(\alpha)) = (\rho(\phi) \circ \rho(\psi))(\alpha), \end{align*} where the third equality uses $\psi(\alpha) \in L^H$ (since $\psi(L^H) = L^H$), so $\rho(\phi)$ is defined at $\psi(\alpha) = \rho(\psi)(\alpha)$. **Kernel.** An element $\phi \in G$ lies in $\ker(\rho)$ if and only if $\phi|_{L^H} = \operatorname{id}_{L^H}$, i.e., $\phi$ fixes $L^H$ pointwise, i.e., $\phi \in \operatorname{Gal}(L/L^H)$. By Part 1, $\operatorname{Gal}(L/L^H) = H$, so $\ker(\rho) = H$. **Surjectivity.** By the first isomorphism theorem for groups, $|\operatorname{im}(\rho)| = |G| / |\ker(\rho)| = |G| / |H|$. From the degree-index formula (Part 1), $|G|/|H| = [G : H] = [L^H : K]$. From Part 2, $L^H/K$ is Galois, so $|\operatorname{Gal}(L^H/K)| = [L^H : K]$. Therefore \begin{align*} |\operatorname{im}(\rho)| = \frac{|G|}{|H|} = [L^H : K] = |\operatorname{Gal}(L^H/K)|. \end{align*} Since $\operatorname{im}(\rho) \subset \operatorname{Gal}(L^H/K)$ and both are finite sets of the same cardinality, $\operatorname{im}(\rho) = \operatorname{Gal}(L^H/K)$, so $\rho$ is surjective. By the first isomorphism theorem, $G/H = G/\ker(\rho) \cong \operatorname{im}(\rho) = \operatorname{Gal}(L^H/K)$, completing Part 3 and the proof.[/step]

[guided]We must construct an explicit isomorphism $G/H \cong \operatorname{Gal}(L^H/K)$. The natural candidate is the restriction map: send each automorphism $\phi \in G$ of $L$ to its restriction $\phi|_{L^H}$. The strategy is to show this map is a well-defined surjective homomorphism with kernel $H$, then invoke the first isomorphism theorem. **Well-definedness.** For $\rho(\phi) = \phi|_{L^H}$ to be an element of $\operatorname{Gal}(L^H/K)$, two conditions must hold: (i) $\phi$ maps $L^H$ to itself, and (ii) $\phi$ fixes $K$. Condition (ii) is immediate: $\phi \in G = \operatorname{Gal}(L/K)$ means $\phi$ fixes $K$ pointwise. Condition (i) is the content of Part 2: since $H \trianglelefteq G$, we proved $\phi(L^H) = L^H$ for every $\phi \in G$. Without normality of $H$, the restriction $\phi|_{L^H}$ might not map $L^H$ to itself, and the homomorphism $\rho$ would not be well-defined. This is precisely why Part 3 requires $H \trianglelefteq G$. **Homomorphism property.** We must verify $\rho(\phi \circ \psi) = \rho(\phi) \circ \rho(\psi)$. For any $\alpha \in L^H$: \begin{align*} \rho(\phi \circ \psi)(\alpha) = (\phi \circ \psi)(\alpha) = \phi(\psi(\alpha)). \end{align*} Since $\psi(L^H) = L^H$, we have $\psi(\alpha) \in L^H$, so $\rho(\psi)(\alpha) = \psi(\alpha)$ and $\rho(\phi)(\psi(\alpha)) = \phi(\psi(\alpha))$. Hence $\rho(\phi \circ \psi)(\alpha) = (\rho(\phi) \circ \rho(\psi))(\alpha)$ for all $\alpha \in L^H$. **Kernel computation.** An automorphism $\phi \in G$ lies in $\ker(\rho)$ precisely when $\phi|_{L^H}$ is the identity on $L^H$, meaning $\phi$ fixes every element of $L^H$. By definition, this says $\phi \in \operatorname{Gal}(L/L^H)$. The identity $\Psi \circ \Phi = \operatorname{id}$ from Part 1 gives $\operatorname{Gal}(L/L^H) = H$. Therefore $\ker(\rho) = H$. **Surjectivity via a cardinality argument.** Rather than constructing preimages directly (which would require extending $L^H$-automorphisms to $L$-automorphisms), we use a counting argument. The first isomorphism theorem for groups gives \begin{align*} |\operatorname{im}(\rho)| = \frac{|G|}{|\ker(\rho)|} = \frac{|G|}{|H|}. \end{align*} From the degree-index formula established in Part 1, $|G|/|H| = [G : H] = [L^H : K]$. From Part 2, $L^H/K$ is Galois (both normal and separable), so $|\operatorname{Gal}(L^H/K)| = [L^H : K]$. Combining: \begin{align*} |\operatorname{im}(\rho)| = \frac{|G|}{|H|} = [L^H : K] = |\operatorname{Gal}(L^H/K)|. \end{align*} Since $\operatorname{im}(\rho) \subset \operatorname{Gal}(L^H/K)$ and both finite sets have the same cardinality, $\operatorname{im}(\rho) = \operatorname{Gal}(L^H/K)$. Hence $\rho$ is surjective. The first isomorphism theorem now gives $G/H = G/\ker(\rho) \cong \operatorname{im}(\rho) = \operatorname{Gal}(L^H/K)$, and the isomorphism is induced by $\rho$: the map $\phi H \mapsto \phi|_{L^H}$ is the desired isomorphism $G/H \xrightarrow{\sim} \operatorname{Gal}(L^H/K)$. This completes Part 3 and the entire proof of the Fundamental Theorem of Galois Theory.[/guided]