[proofplan]
We show that every language in $\mathrm{NP}$ is in $\mathrm{P}$. The Cook-Levin Theorem gives, for each $L \in \mathrm{NP}$, a polynomial-time many-one reduction from $L$ to $\mathrm{SAT}$. If $\mathrm{SAT}$ has a polynomial-time deterministic decider, then composing the reduction with this decider gives a polynomial-time deterministic decider for $L$. Since $L$ was arbitrary, $\mathrm{NP} \subseteq \mathrm{P}$, while $\mathrm{P} \subseteq \mathrm{NP}$ follows because deterministic polynomial-time computation is a special case of nondeterministic polynomial-time computation.
[/proofplan]
[step:Use Cook-Levin to reduce an arbitrary $\mathrm{NP}$ language to $\mathrm{SAT}$]
Let $L \subseteq \{0,1\}^*$ be an arbitrary language with $L \in \mathrm{NP}$. By the Cook-Levin Theorem, there exists a polynomial-time computable many-one reduction
\begin{align*}
f: \{0,1\}^* \to \{0,1\}^*
\end{align*}
from $L$ to $\mathrm{SAT}$. Thus there is a deterministic Turing machine computing $f$ in polynomial time, and for every input string $x \in \{0,1\}^*$,
\begin{align*}
x \in L \iff f(x) \in \mathrm{SAT}.
\end{align*}
[/step]
[step:Compose the reduction with a polynomial-time decider for $\mathrm{SAT}$]
Assume $\mathrm{SAT} \in \mathrm{P}$. Then there exists a deterministic Turing machine $A$ deciding $\mathrm{SAT}$ in polynomial time. Define a deterministic Turing machine $M$ for inputs $x \in \{0,1\}^*$ as follows: first compute $f(x)$, and then run $A$ on the string $f(x)$; accept exactly when $A$ accepts.
For every $x \in \{0,1\}^*$, the correctness of $A$ and the defining property of the reduction give
\begin{align*}
M \text{ accepts } x \iff A \text{ accepts } f(x).
\end{align*}
Since $A$ decides $\mathrm{SAT}$, this is equivalent to
\begin{align*}
f(x) \in \mathrm{SAT}.
\end{align*}
Since $f$ is a many-one reduction from $L$ to $\mathrm{SAT}$, this is equivalent to
\begin{align*}
x \in L.
\end{align*}
Therefore $M$ decides $L$.
[guided]
The goal is to turn a hypothetical fast algorithm for $\mathrm{SAT}$ into a fast algorithm for the arbitrary language $L \in \mathrm{NP}$. The reduction $f$ is the translator: it takes an instance $x$ of the language $L$ and produces a Boolean formula, encoded as a string $f(x)$, such that membership in $L$ is exactly the same as satisfiability of that formula.
Assume $\mathrm{SAT} \in \mathrm{P}$. This means there exists a deterministic Turing machine $A$ whose language is exactly $\mathrm{SAT}$ and whose running time is bounded by a polynomial in the length of its input. We define a new deterministic Turing machine $M$ on input $x \in \{0,1\}^*$ by two deterministic operations: compute $f(x)$, then run $A$ on $f(x)$. The machine $M$ accepts precisely when $A$ accepts.
We now verify correctness, not just plausibility. For every input string $x \in \{0,1\}^*$,
\begin{align*}
M \text{ accepts } x \iff A \text{ accepts } f(x).
\end{align*}
Because $A$ decides $\mathrm{SAT}$, this holds if and only if
\begin{align*}
f(x) \in \mathrm{SAT}.
\end{align*}
Because $f$ is a many-one reduction from $L$ to $\mathrm{SAT}$, the defining equivalence of the reduction gives
\begin{align*}
f(x) \in \mathrm{SAT} \iff x \in L.
\end{align*}
Combining these equivalences gives
\begin{align*}
M \text{ accepts } x \iff x \in L.
\end{align*}
Thus $M$ decides $L$. The important point is that the reduction preserves yes-instances and no-instances exactly; it is not merely a heuristic translation.
[/guided]
[/step]
[step:Verify that the composed decider runs in polynomial time]
Since $f$ is computable in polynomial time, there exist constants $c_f > 0$, $d_f \geq 0$, and $a \in \mathbb{N}$ such that computing $f(x)$ takes at most $c_f |x|^a + d_f$ steps for every $x \in \{0,1\}^*$. In particular, the output length satisfies
\begin{align*}
|f(x)| \leq c_f |x|^a + d_f.
\end{align*}
Since $A$ runs in polynomial time, there exist constants $c_A > 0$, $d_A \geq 0$, and $b \in \mathbb{N}$ such that $A$ runs on every input $y \in \{0,1\}^*$ in at most $c_A |y|^b + d_A$ steps. Therefore the running time of $M$ on input $x$ is bounded by
\begin{align*}
c_f |x|^a + d_f + c_A |f(x)|^b + d_A.
\end{align*}
Using the output-length bound for $f(x)$, this is at most
\begin{align*}
c_f |x|^a + d_f + c_A(c_f |x|^a + d_f)^b + d_A.
\end{align*}
This expression is a polynomial in $|x|$. Hence $M$ is a deterministic polynomial-time decider for $L$, so $L \in \mathrm{P}$.
[/step]
[step:Conclude equality of the complexity classes]
We have shown that every arbitrary language $L \in \mathrm{NP}$ belongs to $\mathrm{P}$. Hence
\begin{align*}
\mathrm{NP} \subseteq \mathrm{P}.
\end{align*}
Conversely,
\begin{align*}
\mathrm{P} \subseteq \mathrm{NP},
\end{align*}
because every deterministic polynomial-time decider is also a nondeterministic polynomial-time decider that ignores its nondeterministic choices. Therefore
\begin{align*}
\mathrm{P}=\mathrm{NP}.
\end{align*}
[/step]
