[proofplan]
We verify directly that the three checklist conditions are exactly the data required for a polynomial-time many-one reduction. The first condition ensures that the output is an admissible instance of the target decision problem. The second condition supplies polynomial-time constructibility of the reduction map, and the third condition proves preservation and reflection of yes-instances. Combining these three facts gives the definition of $A \le_p B$.
[/proofplan]
[step:Use the validity condition to view $f$ as a map from instances of $A$ to instances of $B$]
By hypothesis, $f(x) \in I_B$ for every $x \in I_A$. Hence the same rule defines a map
\begin{align*}
f: I_A \to I_B.
\end{align*}
Thus every valid instance of $A$ is sent to a valid instance of $B$, so the reduction map is well-typed at the level of decision-problem instances.
[/step]
[step:Use the algorithmic condition to prove polynomial-time computability]
By hypothesis, there exist a deterministic algorithm $M$ and a polynomial $p \in \mathbb{N}[t]$ such that, for every valid instance $x \in I_A$, the algorithm $M$ halts on input $x$ within at most $p(|x|)$ steps and outputs $f(x)$. Therefore the map $f: I_A \to I_B$ is computable in time polynomial in the input length $|x|$.
[guided]
The reduction map must be effective, not merely set-theoretic. Hypothesis 2 provides this effectiveness: it gives a deterministic algorithm $M$ which, on input a valid instance $x \in I_A$, produces exactly the string $f(x)$. It also gives a polynomial $p \in \mathbb{N}[t]$ such that the running time of $M$ on input $x$ is bounded above by $p(|x|)$.
Thus the computation time depends polynomially on the length of the input encoding, which is the required complexity bound for a polynomial-time reduction. Since Step 1 already showed that $f(x) \in I_B$ whenever $x \in I_A$, the algorithm does not merely output a string; it outputs a valid instance of the target problem $B$.
[/guided]
[/step]
[step:Use the equivalence condition to prove yes-instance preservation in both directions]
By hypothesis, for every $x \in I_A$,
\begin{align*}
x \in Y_A \iff f(x) \in Y_B.
\end{align*}
The forward implication says that every yes-instance of $A$ is mapped to a yes-instance of $B$. The reverse implication says that if the produced instance is a yes-instance of $B$, then the original instance was a yes-instance of $A$. Equivalently, $f$ preserves the answer to the decision problem on every valid input.
[/step]
[step:Conclude that the checklist gives a polynomial-time many-one reduction]
A polynomial-time many-one reduction from $A$ to $B$ is precisely a polynomial-time computable map from valid instances of $A$ to valid instances of $B$ that preserves the yes/no answer by the equivalence
\begin{align*}
x \in Y_A \iff f(x) \in Y_B.
\end{align*}
Step 1 proves that $f$ maps $I_A$ into $I_B$. Step 2 proves that $f$ is computable in polynomial time. Step 3 proves the required equivalence of yes-instances. Therefore $f$ witnesses $A \le_p B$.
[/step]