Fundamental Theorem of Galois Theory

Step 1 (Artin's lemma gives $L^{\mathrm{Gal}(L/F)}=F$). Let $F$ be an intermediate field, $H=\mathrm{Gal}(L/F)$. Clearly $F\subseteq L^H$ since every $\sigma\in H$ fixes $F$ by definition. For the reverse inclusion, use Artin's theorem: if $H$ is a finite group of automorphisms of $L$ then $[L:L^H]=|H|$; this follows from Dedekind's lemma that distinct field automorphisms are linearly independent as functions $L\to L$, which forces $[L:L^H]\ge|H|$. Since $L/F$ is Galois, $[L:F]=|\mathrm{Gal}(L/F)|=|H|$, and combined with $F\subseteq L^H$, $[L:L^H]=|H|=[L:F]$ we get $F=L^H$.

Step 2 (the two maps are mutually inverse). Given any subgroup $H\le G$, set $F=L^H$; we must show $\mathrm{Gal}(L/F)=H$. By definition $H\subseteq\mathrm{Gal}(L/F)$ (every element of $H$ fixes $L^H=F$). Artin's theorem applied to $H$ gives $[L:F]=[L:L^H]=|H|$. Applying it again to $\mathrm{Gal}(L/F)$ (always valid since $L/F$ is automatically Galois) gives $|\mathrm{Gal}(L/F)|=[L:F]=|H|$. Since $H\subseteq\mathrm{Gal}(L/F)$ and both have the same finite size $|H|$, we get $H=\mathrm{Gal}(L/F)$.

Step 3 (order-reversing). Directly from the definition of fixed field, $H_1\subseteq H_2\Rightarrow L^{H_1}\supseteq L^{H_2}$, so the bijection reverses inclusions in both directions.

Step 4 (degree formulas). We already showed $[L:F]=|\mathrm{Gal}(L/F)|=|H|$. From the tower formula $[L:K]=[L:F][F:K]$ and $[L:K]=|G|$, we get $[F:K]=|G|/|H|=[G:H]$.

Step 5 (normal subgroups correspond to Galois subextensions). For $\sigma\in G$, direct verification gives $\sigma(L^H)=L^{\sigma H\sigma^{-1}}$: indeed $x\in L^H\iff\forall h\in H,\ hx=x\iff\forall h\in H,\ (\sigma h\sigma^{-1})(\sigma x)=\sigma x\iff \sigma x\in L^{\sigma H\sigma^{-1}}$. So $F=L^H$ is stable under every $\sigma\in G$ (which is exactly the normality condition that makes $F/K$ Galois, since $F$ is generated by roots of polynomials over $K$ on which $G$ acts transitively) if and only if $\sigma H\sigma^{-1}=H$ for all $\sigma$, i.e. $H\trianglelefteq G$. In that case restriction $\sigma\mapsto\sigma|_F$ gives a surjective homomorphism $G\to\mathrm{Gal}(F/K)$ with kernel exactly $H$, so $\mathrm{Gal}(F/K)\cong G/H$ by the first isomorphism theorem.