[proofplan]
We first verify that the product poset is locally finite and that every interval in $P\times Q$ factors as a Cartesian product of intervals in $P$ and $Q$. We then define a candidate Möbius function on comparable pairs of $P\times Q$ by multiplying the two coordinate Möbius functions. The defining cancellation recurrence for the Möbius function separates into a product of two finite coordinate sums, and the recurrence uniquely identifies the candidate with $\mu_{P\times Q}$.
[/proofplan]
[step:Show that intervals in the product poset are finite products of coordinate intervals]
Let $(a,b),(c,d)\in P\times Q$ satisfy $(a,b)\le (c,d)$ in the product order. For a poset $R$ and comparable elements $u\le v$ in $R$, write
\begin{align*}
[u,v]_R=\{w\in R:u\le w\le v\}
\end{align*}
By definition of the product order, this means $a\le c$ in $P$ and $b\le d$ in $Q$. The interval from $(a,b)$ to $(c,d)$ in $P\times Q$ is
\begin{align*}
[(a,b),(c,d)]_{P\times Q}=\{(r,s)\in P\times Q:a\le r\le c \text{ and } b\le s\le d\}.
\end{align*}
Hence
\begin{align*}
[(a,b),(c,d)]_{P\times Q}=[a,c]_P\times [b,d]_Q.
\end{align*}
Since $P$ and $Q$ are locally finite, the intervals $[a,c]_P$ and $[b,d]_Q$ are finite. Their Cartesian product is finite, so $P\times Q$ is locally finite.
[/step]
[step:Define the product candidate for the Möbius function]
Let
\begin{align*}
C_{P\times Q}=\{((p_0,q_0),(p_1,q_1))\in (P\times Q)\times(P\times Q):(p_0,q_0)\le(p_1,q_1)\}
\end{align*}
denote the comparable-pair domain of $P\times Q$. Define the map
\begin{align*}
\nu: C_{P\times Q} \to \mathbb{Z}, \qquad ((a,b),(c,d)) \mapsto \mu_P(a,c)\mu_Q(b,d).
\end{align*}
This is well-defined because $(a,b)\le(c,d)$ implies $a\le c$ and $b\le d$, so both $\mu_P(a,c)$ and $\mu_Q(b,d)$ are defined as integers.
We will prove that $\nu$ satisfies the same defining recurrence as the Möbius function of $P\times Q$.
[/step]
[step:Factor the cancellation sum into the two coordinate cancellation sums]
Fix comparable elements $(a,b)\le(c,d)$ in $P\times Q$. Since the interval factors as $[a,c]_P\times[b,d]_Q$, the finite cancellation sum for $\nu$ is
\begin{align*}
\sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))
=
\sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s).
\end{align*}
Because both sums are finite, we may factor the double sum:
\begin{align*}
\sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s)
=
\left(\sum_{r\in [a,c]_P}\mu_P(a,r)\right)
\left(\sum_{s\in [b,d]_Q}\mu_Q(b,s)\right).
\end{align*}
By the Möbius recursion [citetheorem:8101], applied in the locally finite posets $P$ and $Q$, we have
\begin{align*}
\sum_{r\in [a,c]_P}\mu_P(a,r)=
\begin{cases}
1, & a=c,
\end{align*}
\begin{align*}
0, & a<c,
\end{cases}
\end{align*}
and
\begin{align*}
\sum_{s\in [b,d]_Q}\mu_Q(b,s)=
\begin{cases}
1, & b=d,
\end{align*}
\begin{align*}
0, & b<d.
\end{cases}
\end{align*}
Therefore
\begin{align*}
\sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))=
\begin{cases}
1, & (a,b)=(c,d),
\end{align*}
\begin{align*}
0, & (a,b)<(c,d).
\end{cases}
\end{align*}
[guided]
The point of defining $\nu$ as a product is that the interval in the product poset separates into two independent coordinate intervals. Fix $(a,b)\le(c,d)$. From the previous step,
\begin{align*}
[(a,b),(c,d)]_{P\times Q}=[a,c]_P\times[b,d]_Q.
\end{align*}
Thus summing over all intermediate elements $(r,s)$ in the product interval is the same as summing over all $r\in [a,c]_P$ and all $s\in [b,d]_Q$:
\begin{align*}
\sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))
=
\sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s).
\end{align*}
This is a finite double sum because $P$ and $Q$ are locally finite. Since the factor $\mu_P(a,r)$ depends only on $r$ and the factor $\mu_Q(b,s)$ depends only on $s$, finite distributivity gives
\begin{align*}
\sum_{r\in [a,c]_P}\sum_{s\in [b,d]_Q}\mu_P(a,r)\mu_Q(b,s)
=
\left(\sum_{r\in [a,c]_P}\mu_P(a,r)\right)
\left(\sum_{s\in [b,d]_Q}\mu_Q(b,s)\right).
\end{align*}
Now we use exactly the cancellation recurrence that characterizes the Möbius function. By the Möbius recursion [citetheorem:8101], the first coordinate sum is $1$ when $a=c$ and $0$ when $a<c$:
\begin{align*}
\sum_{r\in [a,c]_P}\mu_P(a,r)=
\begin{cases}
1, & a=c,
\end{align*}
\begin{align*}
0, & a<c.
\end{cases}
\end{align*}
The same recurrence in $Q$ gives
\begin{align*}
\sum_{s\in [b,d]_Q}\mu_Q(b,s)=
\begin{cases}
1, & b=d,
\end{align*}
\begin{align*}
0, & b<d.
\end{cases}
\end{align*}
Multiplying these two values handles all cases. If $(a,b)=(c,d)$, then both coordinate sums are $1$, so the product is $1$. If $(a,b)<(c,d)$, then at least one coordinate inequality is strict, so at least one coordinate sum is $0$, and the product is $0$. Hence
\begin{align*}
\sum_{(a,b)\le(r,s)\le(c,d)} \nu((a,b),(r,s))=
\begin{cases}
1, & (a,b)=(c,d),
\end{align*}
\begin{align*}
0, & (a,b)<(c,d).
\end{cases}
\end{align*}
[/guided]
[/step]
[step:Use uniqueness in the Möbius recurrence to identify the candidate]
The preceding step shows that $\nu$ satisfies the defining left cancellation recurrence for the Möbius function on the locally finite poset $P\times Q$. By the uniqueness part of the Möbius recursion [citetheorem:8101], $\nu=\mu_{P\times Q}$ on every comparable pair in $P\times Q$. Therefore, for every $x\le y$ in $P$ and every $u\le v$ in $Q$,
\begin{align*}
\mu_{P\times Q}((x,u),(y,v))=\nu((x,u),(y,v))=\mu_P(x,y)\mu_Q(u,v).
\end{align*}
This is the desired product formula.
[/step]
