If an unary language exists in NPC then P=NP

Let $L$ be an NP-complete unary language. Since $L$ is NP-complete, there is a polytime reduction $f$ from SAT to $L$. Since $f$ is polytime, $|f(x)| \leq C|x|^d$ for some $C,d$. We will now describe a polytime algorithm for SAT.

Denote the input by $\phi$, a formula on the $n$ variables $x_1,\ldots,x_n$; we assume that $|\phi| \geq n$. The algorithm proceeds in $n$ stages, creating a sequence of lists $L_n,\ldots,L_0$. The list $L_k$ consists of a list of pairs $\{(f(\psi_i),\psi_i)\}$, where $\psi_i$ is a formula resulting from substituting values for $x_{k+1},\ldots,x_n$ in $\phi$ and simplifying. We maintain the invariant that $\phi$ is satisfiable if and only if one of the $\psi_i$ is satisfiable.

The initial list $L_n$ consists of the pair $(f(\phi),\phi)$. Given the list $L_k$, we construct the list $L_{k-1}$ in two steps:

1. For each $(f(\psi),\psi) \in L_k)$, add to $L_{k-1}$ the two pairs $(f(\psi|_{x_k=\top}),\psi|_{x_k=\top})$ and $(f(\psi|_{x_k=\bot}),\psi|_{x_k=\bot})$; after substituting a value for $x_k$, we simplify the resulting formula.
2. For each $m$, out of all pairs of the form $(1^m,\psi)$ (if any) retain only one.

It is not hard to check that the invariant is indeed maintained. The final set $L_0$ could potentially contain $(f(\top),\top)$ and $(f(\bot),\bot)$; the formula is satisfiable if and only if it contains the former.

Each list $L_k$ has size at most $C|\phi|^d$, and so the algorithm runs in polynomial time.