[proofplan]
We prove that forcing iteration is associative by writing down the canonical reassociation map on conditions. A left-associated condition consists of a ground condition $p$, a $P$-forcing name $\dot q$ for a $\dot Q$-condition, and a $P * \dot Q$-name $\dot r$ for a $\dot R$-condition; the translation hypothesis converts $\dot r$ into a $P$-name whose interpretations are $\dot Q$-names for $\dot S$-conditions. This allows us to send $((p,\dot q),\dot r)$ to $(p,(\dot q,\dot r^\flat))$, where $\dot r^\flat$ denotes the translated name. We then check that this assignment is well-defined, preserves and reflects the order, and is onto after the same coding convention is imposed on both sides, which is exactly forcing equivalence for the two forcing posets.
[/proofplan]
[step:Fix the translated name convention for third coordinates]
Let $\mathsf{Name}_{P * \dot Q}$ denote the class of $P * \dot Q$-forcing names and let $\mathsf{Name}_{P}(\mathsf{Name}_{\dot Q})$ denote the class of $P$-names whose $P$-generic interpretations are $\dot Q_G$-names. Fix the standard recursive ordered-pair coding of forcing names used in two-step forcing iterations. Let
\begin{align*}
\operatorname{Tr}: \mathsf{Name}_{P * \dot Q} \to \mathsf{Name}_{P}(\mathsf{Name}_{\dot Q})
\end{align*}
denote the standard translation map sending each $P * \dot Q$-name $\dot a$ to a $P$-name $\operatorname{Tr}(\dot a)$ such that
\begin{align*}
(\operatorname{Tr}(\dot a)_G)_H = \dot a_{G * H}
\end{align*}
for every $P$-generic filter $G$ over $M$ and every $\dot Q_G$-generic filter $H$ over $M[G]$.
[claim:Forcing relations are preserved by the two-step name translation]
In the fixed recursive coding of names, $\operatorname{Tr}$ is chosen recursively together with an inverse recoding map on its canonical range: ordered pairs in a $P * \dot Q$-name are replaced rank-by-rank by $P$-names for the corresponding $\dot Q$-names, and the inverse map is defined only on names produced by this recursion. For every formula $\varphi(x_1,\dots,x_n)$ in the forcing language of $P * \dot Q$, every condition $(p,\dot q) \in P * \dot Q$, and every tuple $\dot a_1,\dots,\dot a_n$ of $P * \dot Q$-names,
\begin{align*}
(p,\dot q) \Vdash_{P * \dot Q} \varphi(\dot a_1,\dots,\dot a_n)
\end{align*}
if and only if
\begin{align*}
p \Vdash_P ``\dot q \Vdash_{\dot Q} \varphi(\operatorname{Tr}(\dot a_1),\dots,\operatorname{Tr}(\dot a_n))".
\end{align*}
[/claim]
[proof]
The construction of $\operatorname{Tr}$ is by recursion on the rank of names: each ordered pair appearing in a $P * \dot Q$-name is recoded as a $P$-name whose $P$-generic interpretation is the corresponding $\dot Q_G$-name. The defining property
\begin{align*}
(\operatorname{Tr}(\dot a)_G)_H = \dot a_{G * H}
\end{align*}
therefore follows by induction on the rank of $\dot a$ for every $P$-generic filter $G$ over $M$ and every $\dot Q_G$-generic filter $H$ over $M[G]$. The equivalence of the two forcing assertions follows by induction on the complexity of $\varphi$: atomic membership and equality are exactly the rank-recursion just described, Boolean connectives follow from the recursive definition of forcing, and quantifiers follow because the translation is defined on all $P * \dot Q$-names and has an inverse recoding map on its canonical range. The hypotheses used are precisely that $1_P \Vdash ``\dot Q \text{ is a forcing poset}"$, that $(p,\dot q)$ is a condition in $P * \dot Q$, and that all names being translated are $P * \dot Q$-names.
[/proof]
For a $P * \dot Q$-name $\dot r$, write
\begin{align*}
\dot r^\flat := \operatorname{Tr}(\dot r).
\end{align*}
Thus $\dot r^\flat$ is a $P$-name whose interpretation by a $P$-generic filter is a $\dot Q_G$-name.
The hypothesis on $\dot S$ says exactly that this translation sends the $P * \dot Q$-name $\dot R$ to the $P$-name $\dot S$ for a $\dot Q$-name forcing poset, in the sense that
\begin{align*}
1_P \Vdash_P ``\dot S \text{ is a } \dot Q\text{-name for a forcing poset}"
\end{align*}
and, after generic interpretation,
\begin{align*}
(\dot S_G)_H = \dot R_{G * H}.
\end{align*}
[/step]
[step:Define the reassociation map on conditions]
Define a map between the two forcing iterations
\begin{align*}
\Phi : (P * \dot Q) * \dot R \to P * (\dot Q * \dot S)
\end{align*}
as follows. If $a \in (P * \dot Q) * \dot R$, then $a$ has the form
\begin{align*}
a = ((p,\dot q),\dot r),
\end{align*}
where $p \in P$, $\dot q$ is a $P$-name, and $\dot r$ is a $P * \dot Q$-name. Define $\Phi(a)$ by
\begin{align*}
\Phi(((p,\dot q),\dot r)) := (p,\dot t),
\end{align*}
where $\dot t$ is the $P$-name for the ordered pair
\begin{align*}
\dot t := (\dot q,\dot r^\flat).
\end{align*}
We verify that $\Phi(a)$ is a condition in $P * (\dot Q * \dot S)$. Since $a$ is a condition in $(P * \dot Q) * \dot R$, first
\begin{align*}
p \Vdash_P ``\dot q \in \dot Q",
\end{align*}
and second
\begin{align*}
(p,\dot q) \Vdash_{P * \dot Q} ``\dot r \in \dot R".
\end{align*}
By the forcing-translation lemma just fixed, applied to the formula $x \in \dot R$ and using the hypothesis that $\operatorname{Tr}(\dot R)$ is represented by $\dot S$, the second forcing assertion is equivalent to
\begin{align*}
p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot r^\flat \in \dot S".
\end{align*}
Together these two assertions say precisely that
\begin{align*}
p \Vdash_P ``(\dot q,\dot r^\flat) \in \dot Q * \dot S".
\end{align*}
Therefore $(p,\dot t)$ is a condition in $P * (\dot Q * \dot S)$.
[guided]
The only point needing care is that the third coordinate lives in different syntactic universes on the two sides. On the left, $\dot r$ is a $P * \dot Q$-name. On the right, the second coordinate of $P * (\dot Q * \dot S)$ must be a $P$-name for a condition in the two-step iteration $\dot Q * \dot S$. Therefore we cannot literally write $(p,(\dot q,\dot r))$ unless $\dot r$ has first been recoded as a $P$-name for a $\dot Q$-name.
That is why we define $\dot r^\flat := \operatorname{Tr}(\dot r)$. The translation satisfies
\begin{align*}
(\dot r^\flat_G)_H = \dot r_{G * H}
\end{align*}
for every pair of generics $G$ and $H$. Thus $\dot r^\flat$ is the same mathematical object as $\dot r$ after forcing, but it has the correct syntactic type to appear inside a $P$-name for a $\dot Q * \dot S$-condition.
Now let
\begin{align*}
a = ((p,\dot q),\dot r)
\end{align*}
be a condition in $(P * \dot Q) * \dot R$. By the definition of a two-step iteration, $(p,\dot q)$ must be a condition in $P * \dot Q$, so
\begin{align*}
p \Vdash_P ``\dot q \in \dot Q".
\end{align*}
Again by the definition of the outer iteration, the first coordinate $(p,\dot q)$ must force that the third coordinate is a condition in the forced poset:
\begin{align*}
(p,\dot q) \Vdash_{P * \dot Q} ``\dot r \in \dot R".
\end{align*}
The forcing-translation lemma fixed in the first step applies because $(p,\dot q) \in P * \dot Q$ and $\dot r$ and $\dot R$ are $P * \dot Q$-names. It turns this last assertion into the corresponding internal assertion over $P$:
\begin{align*}
p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot r^\flat \in \dot S".
\end{align*}
Combining the two displayed assertions, $p$ forces that the ordered pair $(\dot q,\dot r^\flat)$ is a condition in the two-step iteration $\dot Q * \dot S$:
\begin{align*}
p \Vdash_P ``(\dot q,\dot r^\flat) \in \dot Q * \dot S".
\end{align*}
Therefore
\begin{align*}
\Phi(((p,\dot q),\dot r)) = (p,(\dot q,\dot r^\flat))
\end{align*}
is a condition of $P * (\dot Q * \dot S)$.
[/guided]
[/step]
[step:Check that reassociation preserves the extension relation]
Let
\begin{align*}
a_1 = ((p_1,\dot q_1),\dot r_1)
\end{align*}
and
\begin{align*}
a_0 = ((p_0,\dot q_0),\dot r_0)
\end{align*}
be conditions in $(P * \dot Q) * \dot R$. By the definition of the order on an iteration,
\begin{align*}
a_1 \leq_{(P * \dot Q) * \dot R} a_0
\end{align*}
holds iff
\begin{align*}
(p_1,\dot q_1) \leq_{P * \dot Q} (p_0,\dot q_0)
\end{align*}
and
\begin{align*}
(p_1,\dot q_1) \Vdash_{P * \dot Q} ``\dot r_1 \leq_{\dot R} \dot r_0".
\end{align*}
Expanding the first condition gives
\begin{align*}
p_1 \leq_P p_0
\end{align*}
and
\begin{align*}
p_1 \Vdash_P ``\dot q_1 \leq_{\dot Q} \dot q_0".
\end{align*}
Translating the third-coordinate comparison gives
\begin{align*}
p_1 \Vdash_P ``\dot q_1 \Vdash_{\dot Q} \dot r_1^\flat \leq_{\dot S} \dot r_0^\flat".
\end{align*}
These three assertions are precisely the definition of
\begin{align*}
(p_1,(\dot q_1,\dot r_1^\flat)) \leq_{P * (\dot Q * \dot S)} (p_0,(\dot q_0,\dot r_0^\flat)).
\end{align*}
Hence
\begin{align*}
a_1 \leq_{(P * \dot Q) * \dot R} a_0
\end{align*}
implies
\begin{align*}
\Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0).
\end{align*}
[/step]
[step:Check that reassociation reflects the extension relation]
Conversely, suppose
\begin{align*}
\Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0).
\end{align*}
Writing out the two images, this means
\begin{align*}
(p_1,(\dot q_1,\dot r_1^\flat)) \leq_{P * (\dot Q * \dot S)} (p_0,(\dot q_0,\dot r_0^\flat)).
\end{align*}
By the definition of the order on $P * (\dot Q * \dot S)$, this is equivalent to
\begin{align*}
p_1 \leq_P p_0,
\end{align*}
\begin{align*}
p_1 \Vdash_P ``\dot q_1 \leq_{\dot Q} \dot q_0",
\end{align*}
and
\begin{align*}
p_1 \Vdash_P ``\dot q_1 \Vdash_{\dot Q} \dot r_1^\flat \leq_{\dot S} \dot r_0^\flat".
\end{align*}
Translating the last assertion back from $P$-names for $\dot Q$-names to $P * \dot Q$-names gives
\begin{align*}
(p_1,\dot q_1) \Vdash_{P * \dot Q} ``\dot r_1 \leq_{\dot R} \dot r_0".
\end{align*}
Together with the first two displayed assertions, this is exactly
\begin{align*}
((p_1,\dot q_1),\dot r_1) \leq_{(P * \dot Q) * \dot R} ((p_0,\dot q_0),\dot r_0).
\end{align*}
Therefore $\Phi$ reflects the order.
[/step]
[step:Identify the inverse map under the same coding convention]
Let $(p,\dot t)$ be a condition in $P * (\dot Q * \dot S)$, presented in the canonical translated-code subposet. By this we mean the dense presentation obtained by replacing each second coordinate by the fixed ordered-pair name supplied by the recursive coding convention, so that
\begin{align*}
p \Vdash_P ``\dot t = (\dot q,\dot s)"
\end{align*}
for some $P$-name $\dot q$ and some $P$-name $\dot s$ which is forced to be a $\dot Q$-name lying in the canonical range of $\operatorname{Tr}$. This replacement by canonical representatives is harmless because the fixed coding is interpretation-preserving in every pair of generics and, by the forcing-translation claim, preserves the order relation. Since $(p,\dot t)$ is a condition,
\begin{align*}
p \Vdash_P ``\dot q \in \dot Q"
\end{align*}
and
\begin{align*}
p \Vdash_P ``\dot q \Vdash_{\dot Q} \dot s \in \dot S".
\end{align*}
Because $\dot s$ lies in the canonical range of $\operatorname{Tr}$, let $\dot s^\sharp$ be the unique inverse translated $P * \dot Q$-name obtained by the inverse recoding map fixed in the first step, so that
\begin{align*}
\operatorname{Tr}(\dot s^\sharp) = \dot s.
\end{align*}
Then the preceding forcing assertion translates to
\begin{align*}
(p,\dot q) \Vdash_{P * \dot Q} ``\dot s^\sharp \in \dot R".
\end{align*}
Let $\mathbb P_{\mathrm{right}}^{\mathrm{can}}$ denote the canonical translated-code subposet of $P * (\dot Q * \dot S)$ described above, and let $\mathbb P_{\mathrm{left}}^{\mathrm{can}}$ denote the corresponding canonical coded presentation of $(P * \dot Q) * \dot R$. Define the map
\begin{align*}
\Psi : \mathbb P_{\mathrm{right}}^{\mathrm{can}} \to \mathbb P_{\mathrm{left}}^{\mathrm{can}}
\end{align*}
by
\begin{align*}
\Psi((p,\dot t)) := ((p,\dot q),\dot s^\sharp).
\end{align*}
The preceding paragraph proves that $\Psi((p,\dot t))$ is a condition in $(P * \dot Q) * \dot R$.
By construction of $\operatorname{Tr}$ and its inverse coding operation, $\Psi(\Phi(((p,\dot q),\dot r))) = ((p,\dot q),\dot r)$ and $\Phi(\Psi((p,\dot t))) = (p,\dot t)$ after replacing names by their standard equivalent codes. Hence $\Phi$ is a bijection between the two coded presentations of the posets.
[/step]
[step:Conclude forcing equivalence from the order isomorphism]
The preceding steps show that $\Phi$ is a bijection and that for all conditions $a_1,a_0 \in (P * \dot Q) * \dot R$,
\begin{align*}
a_1 \leq_{(P * \dot Q) * \dot R} a_0 \iff \Phi(a_1) \leq_{P * (\dot Q * \dot S)} \Phi(a_0).
\end{align*}
Therefore $\Phi$ is an order isomorphism
\begin{align*}
(P * \dot Q) * \dot R \cong P * (\dot Q * \dot S).
\end{align*}
Order-isomorphic forcing posets have exactly corresponding generic filters and hence produce the same forcing extensions. Thus $(P * \dot Q) * \dot R$ and $P * (\dot Q * \dot S)$ are forcing equivalent.
[/step]
