A problem is in NP iff it is solvable by a non-deterministic Turing machine that is guaranteed to run in polynomial time. If such a machine exists, and P==NP, then the problem is also solvable by a deterministic Turing machine in polynomial time.
Strictly speaking, the proof assumes a particular Turing machine. But since universal Turing machines exist, we can equivalently say: if P==NP then there exists a deterministic program that takes a description of a non-deterministic TM and an input string, such that if the non-deterministic TM halts in polynomial time, so does the deterministic algorithm (with the same answer).
(The standard proof of the Cook-Levin theorem assumes that you actually have a polynomial bound on the number of time steps, rather than simply being assured that one exists. This is a technical detail that can be worked around by e.g. doubling the number of steps exponentially until you detect termination.)
Just to make sure I got this right, the basic idea is: simulate the non-deterministic Turing machine using boolean variables, with unconstrained variables for the nondeterministic part. Sort of a symbolic execution on a Turing machine. Convert the simulation to a boolean expression. Convert the boolean expression to 3-SAT form. Put 3-SAT problem into your magical P==NP machine and get an answer out. You've now found the answer given by the nondeterministic Turing machine in polynomial time, if the original would indeed run in polynomial time.
The parts that are "by definition" are:
* the set of programs involving steps like "guess magically" correspond to the ones that can be implemented with at most polynomial slowdown by a non-deterministic Turing machine (this is hand-wavy, but then again we're talking about pseudocode; it's possible to state it more precisely)
* if such an algorithm runs in polynomial time, then it's in NP (by the definition of NP)
* ...so it can be reduced to an instance of any NP-complete problem (by the definition of NP-complete)
* ...and if P=NP then there exists a deterministic, polynomial-time algorithm to solve the problem
The parts that require actual proofs are:
* the fact that the "well-known" examples of NP-complete problems like 3-SAT, TSP, and so on actually correspond to the formal definition of NP. These proofs ultimately reduce to the Cook-Levin theorem, or something similar in spirit.
* the fact that if any problem in NP has a deterministic polynomial-time algorithm, then there is one algorithm that can solve all NP problems in polynomial time. This relies on the existence of universal Turing machines that have at most a polynomial slowdown.
It's likely there are other details that I'm forgetting, but that's the gist of the argument.
And I don't think you were too terse. Thankfully HN makes it easy to see sub-replies to your comments so I saw your reply to 1arity, which was exactly what I needed, and your reply to me capped it off.
Yes, essentially. You stop the simulation after T(n) steps, where T is a polynomial function that depends on the simulation, and reject the input if you haven't accepted by that point. It's clearly in NP as a result.
What would be the yes/no answer for "simulation of a non-deterministic Turing machine"? If it's just "the yes/no answer provided by whatever that Turing machine runs" then that problem is clearly not in NP, since you could easily have some code that takes more than polynomial time. Can you restrict it to "the yes/no answer provided by whatever that Turing machine runs, provided that it runs in polynomial time"?