[proofplan]
We identify the interventional law $P_x(y)$ by repeatedly replacing actions with observations or deleting irrelevant actions using Pearl's do-calculus. First we expand under the intervention $do(X=x)$ over the mediator $Z$ and use the absence of back-door paths from $X$ to $Z$ to identify the mediator law as the observed conditional law. Then we show that the remaining factor $P_x(y\mid z)$ equals $P_z(y)$: observation of $Z=z$ may be exchanged with intervention on $Z=z$, and the intervention on $X$ may then be deleted because $Z$ blocks every directed causal route from $X$ to $Y$. Finally we identify $P_z(y)$ by expanding over $X$, deleting the action on $Z$ from the marginal law of $X$, and exchanging the action $do(Z=z)$ with the observation $Z=z$ conditional on $X=x'$.
[/proofplan]
[step:Expand the interventional outcome law over the mediator]
Fix treatment and outcome values $x$ and $y$. Let
\begin{align*}
S_Z := \operatorname{supp}(Z)
\end{align*}
denote the observational support of $Z$. For each $z\in S_Z$, write
\begin{align*}
P_x(z) := \mathbb P(Z=z \mid do(X=x))
\end{align*}
and, whenever $P_x(z)>0$,
\begin{align*}
P_x(y\mid z) := \mathbb P(Y=y \mid Z=z, do(X=x)).
\end{align*}
By the [law of total probability](/theorems/1113) under the interventional law induced by $do(X=x)$,
\begin{align*}
P_x(y)=\sum_{z\in S_Z} P_x(y\mid z)P_x(z),
\end{align*}
where terms with $P_x(z)=0$ do not affect the sum.
[/step]
[step:Identify the mediator law after intervention on $X$]
By the stated front-door do-calculus condition, $X$ and $Z$ are $m$-separated in the manipulated latent projection $G^*_{\underline X}$, where all directed arrows out of $X$ have been deleted. This is precisely the graph condition in [Pearl's Rule Two](/theorems/9679) [citetheorem:9679] for exchanging the action $do(X=x)$ with the observation $X=x$ when the outcome variable in the rule is $Z$ and there is no background intervention. Therefore
\begin{align*}
P_x(z)=\mathbb P(Z=z \mid X=x)
\end{align*}
for every $z\in S_Z$ for which the displayed [conditional probability](/page/Conditional%20Probability) is defined.
[/step]
[step:Replace conditioning on the mediator by intervention on the mediator]
For $z\in S_Z$ with $P_x(z)>0$, the stated front-door do-calculus condition says that $Y$ and $Z$ are $m$-separated by $X$ in $G^*_{\overline X\underline Z}$, the manipulated latent projection obtained by deleting all directed arrows into $X$ and all directed arrows out of $Z$. This is precisely the graph condition in Pearl's Rule Two [citetheorem:9679] for replacing the observation $Z=z$ by the action $do(Z=z)$ while keeping the background intervention $do(X=x)$ fixed. Applying that rule with action variable $Z$, outcome variable $Y$, and background intervention $do(X=x)$ gives
\begin{align*}
P_x(y\mid z)=P_{x,z}(y),
\end{align*}
where
\begin{align*}
P_{x,z}(y):=\mathbb P(Y=y\mid do(X=x),do(Z=z)).
\end{align*}
[guided]
We want to remove the ordinary conditioning event $Z=z$ from $P_x(y\mid z)$ because the final formula must be written only in terms of observational probabilities. The first move is to turn that observation into an intervention. The manipulated graph relevant to this application of Pearl's Rule Two is $G^*_{\overline X\underline Z}$: the bar over $X$ means that directed arrows into $X$ are deleted, and the underline under $Z$ means that directed arrows out of $Z$ are deleted.
The theorem statement assumes the required separation explicitly: in $G^*_{\overline X\underline Z}$, the variables $Y$ and $Z$ are $m$-separated by $X$. Pearl's Rule Two [citetheorem:9679] states that, under exactly this separation condition, an observation of the action variable may be exchanged with an intervention on that variable. Here the outcome variable in the rule is $Y$, the action variable is $Z$, and the already-fixed intervention is $do(X=x)$. Therefore, for every $z$ for which $P_x(y\mid z)$ is defined,
\begin{align*}
\mathbb P(Y=y \mid Z=z,do(X=x))=\mathbb P(Y=y\mid do(X=x),do(Z=z)).
\end{align*}
Using the shorthand
\begin{align*}
P_{x,z}(y):=\mathbb P(Y=y\mid do(X=x),do(Z=z)),
\end{align*}
this is exactly
\begin{align*}
P_x(y\mid z)=P_{x,z}(y).
\end{align*}
This step is where the front-door graphical separation converts a conditional interventional distribution into a distribution under a joint intervention.
[/guided]
[/step]
[step:Delete the intervention on $X$ after fixing the mediator]
The stated front-door do-calculus condition says that $Y$ and $X$ are $m$-separated by $Z$ in $G^*_{\overline X\overline Z}$, the manipulated latent projection obtained by deleting all directed arrows into $X$ and all directed arrows into $Z$. This is the graph condition in Pearl's Rule Three for deleting the action $do(X=x)$ while retaining the background intervention $do(Z=z)$. Applying [Pearl's Rule Three for deleting actions](/theorems/9680) [citetheorem:9680] gives
\begin{align*}
P_{x,z}(y)=P_z(y),
\end{align*}
where
\begin{align*}
P_z(y):=\mathbb P(Y=y\mid do(Z=z)).
\end{align*}
Combining this identity with the preceding step yields
\begin{align*}
P_x(y\mid z)=P_z(y).
\end{align*}
[/step]
[step:Identify the distribution of $Y$ under intervention on $Z$]
Let
\begin{align*}
S_X := \operatorname{supp}(X)
\end{align*}
denote the observational support of $X$. By the law of total probability under the interventional law induced by $do(Z=z)$,
\begin{align*}
P_z(y)=\sum_{x'\in S_X} P_z(y\mid x')P_z(x'),
\end{align*}
where
\begin{align*}
P_z(x'):=\mathbb P(X=x'\mid do(Z=z))
\end{align*}
and, whenever $P_z(x')>0$,
\begin{align*}
P_z(y\mid x'):=\mathbb P(Y=y\mid X=x',do(Z=z)).
\end{align*}
First, the stated front-door do-calculus condition says that $X$ and $Z$ are $m$-separated in $G^*_{\overline Z}$, the manipulated latent projection obtained by deleting all directed arrows into $Z$. This is the graph condition in Pearl's Rule Three for deleting the action $do(Z=z)$ from the marginal law of $X$. Pearl's Rule Three [citetheorem:9680] gives
\begin{align*}
P_z(x')=\mathbb P(X=x')
\end{align*}
for every $x'\in S_X$.
Second, the stated front-door do-calculus condition says that $Y$ and $Z$ are $m$-separated by $X$ in $G^*_{\underline Z}$, the manipulated latent projection obtained by deleting all directed arrows out of $Z$. This is the graph condition in Pearl's Rule Two for exchanging the action $do(Z=z)$ with the observation $Z=z$ after conditioning on $X=x'$. Pearl's Rule Two [citetheorem:9679] gives
\begin{align*}
P_z(y\mid x')=\mathbb P(Y=y\mid Z=z,X=x')
\end{align*}
for every pair $(z,x')$ for which the displayed conditional probability is defined. Substituting these two identities into the expansion of $P_z(y)$ gives
\begin{align*}
P_z(y)=\sum_{x'\in S_X}\mathbb P(Y=y\mid Z=z,X=x')\mathbb P(X=x').
\end{align*}
[/step]
[step:Combine the identified factors]
Substituting the identities from the previous steps into the mediator expansion gives
\begin{align*}
P_x(y)=\sum_{z\in S_Z} P_x(y\mid z)P_x(z).
\end{align*}
Using
\begin{align*}
P_x(z)=\mathbb P(Z=z\mid X=x)
\end{align*}
and
\begin{align*}
P_x(y\mid z)=P_z(y)=\sum_{x'\in S_X}\mathbb P(Y=y\mid Z=z,X=x')\mathbb P(X=x'),
\end{align*}
we obtain
\begin{align*}
P_x(y)=\sum_{z\in S_Z}\mathbb P(Z=z\mid X=x)\sum_{x'\in S_X}\mathbb P(Y=y\mid Z=z,X=x')\mathbb P(X=x').
\end{align*}
Since $S_Z=\operatorname{supp}(Z)$ and $S_X=\operatorname{supp}(X)$ by definition, this is the stated front-door formula. In the continuous or mixed case, the same argument is performed with regular conditional probability kernels; the displayed sums are replaced by the corresponding integrals against the conditional kernel of $Z$ given $X=x$ and the marginal law of $X$.
[/step]
