[proofplan]
We sandwich $\mathcal{O}_L$ between two free $\mathcal{O}_K$-modules of rank $n$ using the equivalence of norms on $L$ as a finite-dimensional $K$-vector space. Choosing a $K$-basis of $L$, the max norm and the extended absolute value are equivalent, so the unit ball $\mathcal{O}_L$ with respect to one norm is trapped between scaled copies of the unit ball with respect to the other. Since $\mathcal{O}_K$ is a PID, a torsion-free module sandwiched between free modules of the same rank is itself free of that rank. We then verify completeness and finiteness of the residue field to conclude $L$ is a local field.
[/proofplan]
[step:Choose a $K$-basis of $L$ and establish norm equivalence]
Let $L/K$ be a finite extension of degree $n = [L:K]$, and let $|\cdot|_L$ denote the unique extension of the absolute value from $K$ to $L$ (given by $|\alpha|_L = |N_{L/K}(\alpha)|^{1/n}$, whose existence and uniqueness is guaranteed by the [Unique Extension of Absolute Values to Finite Extensions](/theorems/???)).
Choose a $K$-basis $\alpha_1, \ldots, \alpha_n$ of $L$. Define the max norm on $L$ by
\begin{align*}
\left\|\sum_{i=1}^n x_i \alpha_i\right\|_{\max} := \max_{1 \leq i \leq n} |x_i| \quad \text{for } x_i \in K.
\end{align*}
Both $|\cdot|_L$ and $\|\cdot\|_{\max}$ are norms on $L$ viewed as a finite-dimensional $K$-vector space. By the [All Norms on a Finite-Dimensional Complete Valued Space Are Equivalent](/theorems/???), there exist constants $C, D > 0$ such that
\begin{align*}
C \cdot \|x\|_{\max} \leq |x|_L \leq D \cdot \|x\|_{\max} \quad \text{for all } x \in L.
\end{align*}
[guided]
The equivalence of norms theorem requires $K$ to be complete and non-archimedean. Here $K$ is a local field, hence complete. The theorem provides constants $C, D > 0$ depending on the basis $\{\alpha_1, \ldots, \alpha_n\}$.
We can arrange for $C$ and $D$ to have the form $|b|$ and $|a|^{-1}$ respectively, for elements $a, b \in K^\times$. This is because the value group $|K^\times|$ is dense enough in $\mathbb{R}_{>0}$ (or discrete, in which case we round to the nearest value).
[/guided]
[/step]
[step:Sandwich $\mathcal{O}_L$ between two free $\mathcal{O}_K$-modules of rank $n$]
Since the constants $C, D$ lie in $\mathbb{R}_{>0}$ and $|K^\times| = \{|\pi_K|^m : m \in \mathbb{Z}\}$ is a discrete subgroup of $\mathbb{R}_{>0}$, we can choose $a, b \in K^\times$ such that $|a| \geq D$ and $|b| \leq C$. Then for any $x = \sum x_i \alpha_i \in L$:
\begin{align*}
|x|_L \leq 1 \implies \|x\|_{\max} \leq C^{-1} \leq |b|^{-1} \implies x_i \in b^{-1}\mathcal{O}_K \text{ for all } i,
\end{align*}
and
\begin{align*}
\|x\|_{\max} \leq |a|^{-1} \implies |x|_L \leq D \cdot |a|^{-1} \leq 1 \implies x \in \mathcal{O}_L.
\end{align*}
Setting $\beta_i = a^{-1}\alpha_i$ and $\gamma_i = b^{-1}\alpha_i$, this gives the inclusions
\begin{align*}
\bigoplus_{i=1}^n \mathcal{O}_K \beta_i \subseteq \mathcal{O}_L \subseteq \bigoplus_{i=1}^n \mathcal{O}_K \gamma_i.
\end{align*}
Both the left and right modules are free $\mathcal{O}_K$-modules of rank $n$.
[guided]
The left inclusion says: if $\max_i |x_i| \leq |a|^{-1}$, i.e., all $x_i \in a^{-1}\mathcal{O}_K$, then $|\sum x_i \alpha_i|_L \leq D \cdot |a|^{-1} \leq 1$, so $\sum x_i \alpha_i \in \mathcal{O}_L$. This means $\bigoplus \mathcal{O}_K (a^{-1}\alpha_i) \subseteq \mathcal{O}_L$.
The right inclusion says: if $|\sum x_i \alpha_i|_L \leq 1$, then $\max_i |x_i| \leq C^{-1} \leq |b|^{-1}$, so $x_i \in b^{-1}\mathcal{O}_K$ for all $i$. This means $\mathcal{O}_L \subseteq \bigoplus \mathcal{O}_K (b^{-1}\alpha_i)$.
The key point is that both bounding modules are free of the same rank $n$.
[/guided]
[/step]
[step:Deduce $\mathcal{O}_L$ is free of rank $n$ over $\mathcal{O}_K$]
The ring $\mathcal{O}_K$ is a PID (it is a DVR with unique prime $\pi_K$). The module $\mathcal{O}_L$ is torsion-free as an $\mathcal{O}_K$-module: if $c \cdot x = 0$ with $c \in \mathcal{O}_K \setminus \{0\}$ and $x \in \mathcal{O}_L$, then $x = 0$ since $\mathcal{O}_L$ is an integral domain.
By the structure theorem for finitely generated modules over a PID, a torsion-free submodule of a free module of rank $n$ over a PID is free of rank at most $n$. Since $\mathcal{O}_L$ is sandwiched between free modules of rank $n$, it is finitely generated (as a submodule of the Noetherian module $\bigoplus \mathcal{O}_K \gamma_i$), torsion-free, and contains a free submodule of rank $n$ (namely $\bigoplus \mathcal{O}_K \beta_i$). Therefore $\operatorname{rank}_{\mathcal{O}_K}(\mathcal{O}_L) = n$, and $\mathcal{O}_L$ is a free $\mathcal{O}_K$-module of rank $n$.
[/step]
[step:Verify that $L$ is a local field]
We must check that $L$ is complete with a finite residue field.
**Completeness.** $L$ is a finite-dimensional vector space over the complete field $K$. By the [All Norms on a Finite-Dimensional Complete Valued Space Are Equivalent](/theorems/???), $L$ is complete under $|\cdot|_L$.
**Finite residue field.** The residue field $k_L = \mathcal{O}_L / \mathfrak{m}_L$ is a finite extension of $k_K = \mathcal{O}_K / \mathfrak{m}_K$. Since $\mathcal{O}_L$ is generated by $n$ elements over $\mathcal{O}_K$, the residue field $k_L$ is generated by at most $n$ elements over $k_K$. Therefore $[k_L : k_K] \leq n < \infty$. Since $k_K$ is finite (as $K$ is a local field), $k_L$ is also finite.
**Discrete valuation.** The value group of $L$ satisfies $|L^\times|_L \subseteq (|K^\times|)^{1/n} = \{|\pi_K|^{m/n} : m \in \mathbb{Z}\}$. This is a discrete subgroup of $\mathbb{R}_{>0}$, so the valuation $v_L = -\log_{|\pi_L|} |\cdot|_L$ is discrete (i.e., $v_L(L^\times) = \mathbb{Z}$, after normalizing). Therefore $L$ is a local field.
[guided]
**Why is the valuation discrete?** The value group $w(L^\times)$ (where $w = -\log_p |\cdot|_L$) is contained in $\frac{1}{n}\mathbb{Z}$, because $w(\alpha) = \frac{1}{n} v_K(N_{L/K}(\alpha))$ and $v_K(N_{L/K}(\alpha)) \in \mathbb{Z}$ for all $\alpha \in L^\times$. The group $\frac{1}{n}\mathbb{Z}$ is discrete in $\mathbb{R}$, so $w(L^\times)$ is discrete. In particular, $w(L^\times) = \frac{1}{e}\mathbb{Z}$ for some positive integer $e$ dividing $n$, and this $e$ is the ramification index $e_{L/K}$.
**Why does $[k_L : k_K] \leq n$?** The surjection $\mathcal{O}_L \twoheadrightarrow k_L$ restricts to a surjection $\bigoplus_{i=1}^n \mathcal{O}_K \gamma_i \twoheadrightarrow k_L$ (since $\mathcal{O}_L \subseteq \bigoplus \mathcal{O}_K \gamma_i$). Reducing modulo $\mathfrak{m}_K$ gives a surjection $k_K^n \twoheadrightarrow k_L$ (more precisely, the images of $\gamma_1, \ldots, \gamma_n$ in $k_L$ span $k_L$ over $k_K$). So $[k_L : k_K] \leq n$.
[/guided]
[/step]
