[proofplan]
We verify the three claims in turn. Part (i) is a direct check that $\|\cdot\|_{X/Y}$ is well-defined on cosets and satisfies the three norm axioms; positive definiteness uses that $Y$ is *closed*, so $\operatorname{dist}(x, Y) = 0$ forces $x \in Y$. Part (ii) shows $q$ is contractive ($\|q\| \le 1$) by taking $y = 0$ in the infimum, and shows $q$ maps the open unit ball $D_X$ onto $D_{X/Y}$ by exhibiting a representative of norm $< 1$ for any coset of norm $< 1$. Part (iii) uses the standard subsequence trick: a Cauchy sequence in $X/Y$ has a subsequence with rapidly decreasing differences, which can be lifted to a Cauchy sequence in $X$ via the surjectivity of $q$ on small balls; completeness of $X$ then gives a limit, whose image in $X/Y$ is the limit of the original Cauchy sequence.
[/proofplan]
[step:Verify the quotient norm is well-defined on cosets]
Define
\begin{align*}
\|\cdot\|_{X/Y}: X/Y &\to \mathbb{R}, \\
x + Y &\mapsto \operatorname{dist}(x, Y) = \inf_{y \in Y}\|x + y\|_X.
\end{align*}
**Well-definedness.** Suppose $x + Y = x' + Y$, i.e. $x - x' \in Y$. Then for any $y \in Y$, $y + (x - x') \in Y$ and $\|x + y\|_X = \|x' + (y + (x - x'))\|_X$. Taking the infimum over $y \in Y$ on the left and noting the map $y \mapsto y + (x - x')$ is a bijection $Y \to Y$:
\begin{align*}
\inf_{y \in Y}\|x + y\|_X = \inf_{y' \in Y}\|x' + y'\|_X,
\end{align*}
so $\operatorname{dist}(x, Y) = \operatorname{dist}(x', Y)$. The function $\|\cdot\|_{X/Y}$ depends only on the coset, not the representative.
[/step]
[step:Verify positive definiteness using that $Y$ is closed]
We have $\|x + Y\|_{X/Y} = \inf_{y \in Y}\|x + y\|_X \ge 0$ since each $\|x + y\|_X \ge 0$.
If $x + Y = 0_{X/Y} = 0 + Y$, then $x \in Y$, and taking $y = -x \in Y$ gives $\|x + y\|_X = 0$, so $\|x + Y\|_{X/Y} = 0$.
Conversely, suppose $\|x + Y\|_{X/Y} = 0$, i.e. $\operatorname{dist}(x, Y) = 0$. Then there is a sequence $(y_n) \subseteq Y$ with $\|x + y_n\|_X \to 0$, equivalently $-y_n \to x$ in $X$. Since $-y_n \in Y$ for each $n$ (as $Y$ is a subspace, hence closed under negation) and $Y$ is closed in $X$, the limit $x$ lies in $Y$. Hence $x + Y = 0 + Y$, the zero element of $X/Y$.
[guided]
This is the only place in the proof where the **closedness** hypothesis on $Y$ is consumed. If $Y$ were not closed, then for any $x \in \overline{Y} \setminus Y$ we would have $\operatorname{dist}(x, Y) = 0$ but $x + Y \ne 0$ in $X/Y$, so $\|\cdot\|_{X/Y}$ would only be a *semi-norm*, not a norm.
The argument: $\operatorname{dist}(x, Y) = 0$ means there are $y_n \in Y$ with $\|x + y_n\|_X \to 0$, i.e. $-y_n \to x$ in $X$. The sequence $(-y_n)$ lies in $Y$ (closed under negation since $Y$ is a subspace), so its limit $x$ lies in $\overline{Y} = Y$. Hence $x \in Y$ and $x + Y = 0 + Y$ in $X/Y$. Without closedness, the limit $x$ would only be guaranteed to lie in $\overline{Y}$, which need not equal $Y$.
[/guided]
[/step]
[step:Verify absolute homogeneity]
Let $t \in \mathbb{F}$ and $x + Y \in X/Y$. By definition of scalar multiplication on the quotient, $t(x + Y) = (tx) + Y$.
If $t = 0$: $0 \cdot (x + Y) = 0 + Y$ has norm $0 = |0| \cdot \|x + Y\|_{X/Y}$.
If $t \ne 0$: the map $y \mapsto y/t$ is a bijection $Y \to Y$ (since $Y$ is a subspace, closed under scalar multiplication). Hence
\begin{align*}
\|t(x + Y)\|_{X/Y} = \inf_{y \in Y}\|tx + y\|_X = \inf_{y \in Y}\bigl(|t|\,\|x + y/t\|_X\bigr) = |t|\, \inf_{y' \in Y}\|x + y'\|_X = |t|\,\|x + Y\|_{X/Y},
\end{align*}
where the second equality uses absolute homogeneity of $\|\cdot\|_X$ with $\|tx + y\|_X = |t|\,\|x + y/t\|_X$, and the third equality substitutes $y' = y/t$.
[/step]
[step:Verify the triangle inequality]
Let $x_1 + Y$, $x_2 + Y \in X/Y$. For any $y_1, y_2 \in Y$, the element $y_1 + y_2 \in Y$, and the triangle inequality of $\|\cdot\|_X$ gives
\begin{align*}
\|(x_1 + x_2) + (y_1 + y_2)\|_X = \|(x_1 + y_1) + (x_2 + y_2)\|_X \le \|x_1 + y_1\|_X + \|x_2 + y_2\|_X.
\end{align*}
Since $y_1 + y_2 \in Y$, the left side is bounded below by $\inf_{y \in Y}\|(x_1 + x_2) + y\|_X = \|(x_1 + x_2) + Y\|_{X/Y}$. Hence
\begin{align*}
\|(x_1 + x_2) + Y\|_{X/Y} \le \|x_1 + y_1\|_X + \|x_2 + y_2\|_X \qquad \text{for all } y_1, y_2 \in Y.
\end{align*}
Taking the infimum over $y_1$ then over $y_2$ on the right yields
\begin{align*}
\|(x_1 + x_2) + Y\|_{X/Y} \le \|x_1 + Y\|_{X/Y} + \|x_2 + Y\|_{X/Y}.
\end{align*}
This completes the verification that $\|\cdot\|_{X/Y}$ is a norm on $X/Y$, proving (i).
[/step]
[step:Verify $q$ is linear, surjective, and bounded with $\|q\| \le 1$]
Define
\begin{align*}
q: X &\to X/Y, \\
x &\mapsto x + Y.
\end{align*}
**Linearity.** For $x_1, x_2 \in X$ and scalars $\lambda_1, \lambda_2$:
\begin{align*}
q(\lambda_1 x_1 + \lambda_2 x_2) = (\lambda_1 x_1 + \lambda_2 x_2) + Y = \lambda_1 (x_1 + Y) + \lambda_2 (x_2 + Y) = \lambda_1 q(x_1) + \lambda_2 q(x_2),
\end{align*}
using the definition of vector operations on the quotient.
**Surjectivity.** For any $x + Y \in X/Y$, $q(x) = x + Y$.
**Boundedness with $\|q\| \le 1$.** Taking $y = 0 \in Y$ in the infimum,
\begin{align*}
\|q(x)\|_{X/Y} = \inf_{y \in Y}\|x + y\|_X \le \|x + 0\|_X = \|x\|_X,
\end{align*}
so $q \in \mathcal{L}(X, X/Y)$ with $\|q\| \le 1$.
[/step]
[step:Show $q$ maps $D_X$ onto $D_{X/Y}$ to establish $\|q\| = 1$ and openness]
Let $D_X := \{x \in X : \|x\|_X < 1\}$ and $D_{X/Y} := \{\xi \in X/Y : \|\xi\|_{X/Y} < 1\}$ denote the *open* unit balls.
**$q(D_X) \subseteq D_{X/Y}$.** If $x \in D_X$ then $\|q(x)\|_{X/Y} \le \|x\|_X < 1$, so $q(x) \in D_{X/Y}$.
**$D_{X/Y} \subseteq q(D_X)$.** Let $\xi \in D_{X/Y}$ and pick any representative $x \in X$ with $\xi = x + Y$. Then $\operatorname{dist}(x, Y) = \|\xi\|_{X/Y} < 1$. By definition of infimum, there exists $y \in Y$ with $\|x + y\|_X < 1$. Set $x' := x + y$; then $x' \in D_X$ and
\begin{align*}
q(x') = q(x + y) = q(x) + q(y) = q(x) + 0 = \xi,
\end{align*}
since $q(y) = y + Y = 0 + Y$ for $y \in Y$. Hence $\xi \in q(D_X)$.
This proves $q(D_X) = D_{X/Y}$.
**$\|q\| = 1$.** We have assumed $Y \subsetneq X$. Fix $c \in (0, 1)$. Pick $x_0 \in X \setminus Y$; since $Y$ is closed, $\operatorname{dist}(x_0, Y) > 0$, so $\|q(x_0)\|_{X/Y} > 0$. Set
\begin{align*}
\xi := \frac{c}{\|q(x_0)\|_{X/Y}}\, q(x_0) \in X/Y, \qquad \text{which satisfies } \|\xi\|_{X/Y} = c < 1.
\end{align*}
By the inclusion $D_{X/Y} \subseteq q(D_X)$ proved above, there exists $x \in D_X$ with $q(x) = \xi$. Then $\|x\|_X < 1$ and
\begin{align*}
\|q\| \ge \frac{\|q(x)\|_{X/Y}}{\|x\|_X} = \frac{c}{\|x\|_X} > c.
\end{align*}
Since $c \in (0, 1)$ was arbitrary, $\|q\| \ge 1$. Combined with $\|q\| \le 1$ from the previous step, $\|q\| = 1$.
**Openness.** A linear map $q: X \to X/Y$ is open iff it sends the open unit ball $D_X$ to a set containing an open neighbourhood of $0$ in $X/Y$. We have shown $q(D_X) = D_{X/Y}$, the open unit ball of $X/Y$. By translation and scaling (using linearity and absolute homogeneity), $q$ sends every open ball $B(x_0, r)$ in $X$ onto the open ball $B(q(x_0), r)$ in $X/Y$. Hence the image of every open set under $q$ is open: $q$ is an open map.
This proves (ii).
[/step]
[step:Reduce the completeness of $X/Y$ to a Cauchy lifting argument]
Assume $X$ is a Banach space. Let $(\xi_n) = (x_n + Y)$ be a Cauchy sequence in $X/Y$. To prove $X/Y$ is Banach, we must produce a limit $\xi \in X/Y$.
**Pass to a fast subsequence.** Since $(\xi_n)$ is Cauchy, we may extract a subsequence $(\xi_{n_k})_{k \ge 1}$ with
\begin{align*}
\|\xi_{n_{k+1}} - \xi_{n_k}\|_{X/Y} < 2^{-k} \qquad \text{for all } k \ge 1.
\end{align*}
This is a standard consequence of the Cauchy condition: choose $n_1$ so that $\|\xi_n - \xi_{n_1}\|_{X/Y} < 2^{-1}$ for all $n \ge n_1$, then $n_2 > n_1$ with $\|\xi_n - \xi_{n_2}\|_{X/Y} < 2^{-2}$ for all $n \ge n_2$, etc.
[guided]
The strategy in any "Cauchy implies convergent" argument in a quotient space is: lift the Cauchy sequence in the quotient to a Cauchy sequence in the original space, take its limit there, and project back. The challenge is that the natural lift — choosing an arbitrary representative $x_n \in \xi_n$ — is *not* Cauchy in $X$ in general, because the choice of representative is not coordinated across different $n$.
The fix is to **lift the differences**, not the sequence itself. Each successive difference $\xi_{n_{k+1}} - \xi_{n_k}$ is a coset of small norm, so by the surjectivity of $q$ on small open balls (proved in the openness step), we can lift it to a vector in $X$ of similarly small norm. Summing these telescopic differences from a fixed starting representative produces a Cauchy sequence in $X$ that projects onto the (sub)sequence in $X/Y$.
Why pass to a subsequence with $\|\xi_{n_{k+1}} - \xi_{n_k}\|_{X/Y} < 2^{-k}$? Because then the lifted differences in $X$ have norms summable by a geometric series $\sum 2^{-k} < \infty$, which is exactly the condition for the cumulative sum to be Cauchy. A general Cauchy sequence has differences only "eventually small," not summable, so the subsequence trick is essential.
[/guided]
[/step]
[step:Lift the fast subsequence to a Cauchy sequence in $X$]
Choose any representative $z_1 \in X$ with $z_1 + Y = \xi_{n_1}$.
Inductively, suppose $z_1, \ldots, z_k \in X$ have been chosen with $z_j + Y = \xi_{n_j}$ for $j = 1, \ldots, k$. The element $\xi_{n_{k+1}} - \xi_{n_k} \in X/Y$ has norm $< 2^{-k}$. By the surjectivity of $q$ on the open ball $D_{X/Y}^{(2^{-k})} = \{\eta \in X/Y : \|\eta\|_{X/Y} < 2^{-k}\}$ — which follows from the openness step by scaling: $q$ maps $\{x \in X : \|x\|_X < 2^{-k}\}$ onto $D_{X/Y}^{(2^{-k})}$ — there exists $w_k \in X$ with $\|w_k\|_X < 2^{-k}$ and $w_k + Y = \xi_{n_{k+1}} - \xi_{n_k}$. Set
\begin{align*}
z_{k+1} := z_k + w_k.
\end{align*}
Then $z_{k+1} + Y = (z_k + Y) + (w_k + Y) = \xi_{n_k} + (\xi_{n_{k+1}} - \xi_{n_k}) = \xi_{n_{k+1}}$, and $\|z_{k+1} - z_k\|_X = \|w_k\|_X < 2^{-k}$.
**$(z_k)$ is Cauchy in $X$.** For $m > k$,
\begin{align*}
\|z_m - z_k\|_X = \biggl\|\sum_{j=k}^{m-1}(z_{j+1} - z_j)\biggr\|_X \le \sum_{j=k}^{m-1}\|z_{j+1} - z_j\|_X < \sum_{j=k}^{m-1} 2^{-j} < 2^{-k+1}.
\end{align*}
This bound tends to $0$ as $k \to \infty$, so $(z_k)$ is Cauchy.
[/step]
[step:Take the limit in $X$ and conclude convergence in $X/Y$]
Since $X$ is a Banach space, the Cauchy sequence $(z_k)$ has a limit $z \in X$: $z_k \to z$ in $\|\cdot\|_X$.
Apply $q$, which is bounded (hence continuous) by the earlier step:
\begin{align*}
\xi_{n_k} = z_k + Y = q(z_k) \xrightarrow{k \to \infty} q(z) = z + Y.
\end{align*}
Setting $\xi := z + Y \in X/Y$, the subsequence $(\xi_{n_k})$ converges to $\xi$ in $X/Y$.
Since $(\xi_n)$ is Cauchy in $X/Y$ and has a convergent subsequence with limit $\xi$, the full sequence $(\xi_n)$ also converges to $\xi$. We supply the short argument for completeness: given $\varepsilon > 0$, choose $N_1$ such that $\|\xi_m - \xi_n\|_{X/Y} < \varepsilon/2$ for all $m, n \ge N_1$ (Cauchy), and choose $K$ such that $n_K \ge N_1$ and $\|\xi_{n_K} - \xi\|_{X/Y} < \varepsilon/2$ (subsequence convergence). For $n \ge N_1$, the triangle inequality yields $\|\xi_n - \xi\|_{X/Y} \le \|\xi_n - \xi_{n_K}\|_{X/Y} + \|\xi_{n_K} - \xi\|_{X/Y} < \varepsilon$.
Hence every Cauchy sequence in $X/Y$ converges, proving $X/Y$ is a Banach space and establishing (iii).
[/step]
[step:Assemble the conclusion]
Steps one through four prove (i): $\|\cdot\|_{X/Y}$ is well-defined on cosets, positive definite (using closedness of $Y$), absolutely homogeneous, and satisfies the triangle inequality.
Steps five and six prove (ii): $q$ is linear, surjective, has $\|q\| = 1$, maps $D_X$ onto $D_{X/Y}$, and is open.
Steps seven through nine prove (iii) by lifting a fast subsequence of any Cauchy sequence in $X/Y$ to a Cauchy sequence in $X$, taking its limit, and projecting back.
All three claims of the theorem are established.
[/step]
