[proofplan] We prove the Möbius formula by defining the proposed product expression on every comparable pair of $P\times Q$ and checking the recursive defining identities for the Möbius function. The key point is that an interval in the product poset is exactly the product of the corresponding intervals, so the finite Möbius sum over the product factors into two finite sums. The rank [generating function identity](/theorems/2212) then follows by expanding the defining sum over all pairs and using additivity of rank in the product. [/proofplan]

[step:Identify intervals in the product poset]Fix $x_1,y_1\in P$ and $x_2,y_2\in Q$ with $x_1\le_P y_1$ and $x_2\le_Q y_2$. Define the intervals \begin{align*} [x_1,y_1]_P=\{z_1\in P:x_1\le_P z_1\le_P y_1\} \end{align*} and \begin{align*} [x_2,y_2]_Q=\{z_2\in Q:x_2\le_Q z_2\le_Q y_2\}. \end{align*} By the definition of the product order, an element $(z_1,z_2)\in P\times Q$ satisfies \begin{align*} (x_1,x_2)\le_{P\times Q}(z_1,z_2)\le_{P\times Q}(y_1,y_2) \end{align*} if and only if $z_1\in [x_1,y_1]_P$ and $z_2\in [x_2,y_2]_Q$. Hence \begin{align*} [(x_1,x_2),(y_1,y_2)]_{P\times Q} = [x_1,y_1]_P\times [x_2,y_2]_Q. \end{align*}[/step]

[guided]The product order is componentwise, so inequalities in $P\times Q$ split into two independent inequalities. More explicitly, the relation \begin{align*} (x_1,x_2)\le_{P\times Q}(z_1,z_2)\le_{P\times Q}(y_1,y_2) \end{align*} means simultaneously \begin{align*} x_1\le_P z_1\le_P y_1 \end{align*} and \begin{align*} x_2\le_Q z_2\le_Q y_2. \end{align*} Thus choosing an element of the interval in $P\times Q$ is exactly the same as choosing one element of $[x_1,y_1]_P$ and one element of $[x_2,y_2]_Q$. This gives the interval identity \begin{align*} [(x_1,x_2),(y_1,y_2)]_{P\times Q} = [x_1,y_1]_P\times [x_2,y_2]_Q. \end{align*} This identity is the reason the Möbius sum in the next step factors into two separate sums.[/guided]

[step:Verify the Möbius recursion for the product formula] Define the set of comparable pairs in $P\times Q$ by \begin{align*} \mathcal C_{P\times Q}=\{(u,v)\in (P\times Q)\times(P\times Q):u\le_{P\times Q}v\}. \end{align*} Define a function $M:\mathcal C_{P\times Q}\to \mathbb Z$ by \begin{align*} M\bigl((a_1,a_2),(b_1,b_2)\bigr)=\mu_P(a_1,b_1)\mu_Q(a_2,b_2) \end{align*} whenever $a_1\le_P b_1$ and $a_2\le_Q b_2$. We show that $M$ satisfies the defining recursion of the Möbius function of $P\times Q$. First, for every $(a_1,a_2)\in P\times Q$, \begin{align*} M\bigl((a_1,a_2),(a_1,a_2)\bigr) = \mu_P(a_1,a_1)\mu_Q(a_2,a_2) = 1\cdot 1 = 1. \end{align*} Now suppose \begin{align*} (x_1,x_2)<_{P\times Q}(y_1,y_2). \end{align*} Then at least one of $x_1<_P y_1$ or $x_2<_Q y_2$ holds. Using the interval identity from the previous step and finiteness of the intervals, we obtain \begin{align*} \sum_{(x_1,x_2)\le_{P\times Q} (z_1,z_2)\le_{P\times Q} (y_1,y_2)} M\bigl((x_1,x_2),(z_1,z_2)\bigr)=\sum_{z_1\in [x_1,y_1]_P}\sum_{z_2\in [x_2,y_2]_Q}\mu_P(x_1,z_1)\mu_Q(x_2,z_2). \end{align*} Because the sums are finite, the double sum factors: \begin{align*} \sum_{z_1\in [x_1,y_1]_P}\sum_{z_2\in [x_2,y_2]_Q}\mu_P(x_1,z_1)\mu_Q(x_2,z_2)=\left(\sum_{z_1\in [x_1,y_1]_P}\mu_P(x_1,z_1)\right)\left(\sum_{z_2\in [x_2,y_2]_Q}\mu_Q(x_2,z_2)\right). \end{align*} The defining recursion for $\mu_P$ gives $\sum_{z_1\in [x_1,y_1]_P}\mu_P(x_1,z_1)=1$ when $x_1=y_1$, and gives \begin{align*} \sum_{z_1\in [x_1,y_1]_P}\mu_P(x_1,z_1) = 0 \end{align*} when $x_1<_P y_1$. The analogous identity holds in $Q$. Since at least one coordinate inequality is strict, one of the two factors is $0$. Therefore \begin{align*} \sum_{(x_1,x_2)\le_{P\times Q} (z_1,z_2)\le_{P\times Q} (y_1,y_2)} M\bigl((x_1,x_2),(z_1,z_2)\bigr) = 0. \end{align*} Thus $M$ satisfies the Möbius recursion on $P\times Q$. Since $P\times Q$ is finite, the hypotheses of [citetheorem:8101] apply to the finite poset $P\times Q$, and the converse uniqueness statement in that theorem says that these recursive equations determine the Möbius function uniquely. Therefore \begin{align*} M=\mu_{P\times Q}. \end{align*} Evaluating at $((x_1,x_2),(y_1,y_2))$ gives \begin{align*} \mu_{P\times Q}\bigl((x_1,x_2),(y_1,y_2)\bigr) = \mu_P(x_1,y_1)\mu_Q(x_2,y_2). \end{align*} [/step]

[step:Factor the rank generating function by additivity of rank] Assume now that $P$ and $Q$ are ranked with rank functions $\operatorname{rk}_P$ and $\operatorname{rk}_Q$, and that $P\times Q$ has rank function \begin{align*} \operatorname{rk}_{P\times Q}(p,q)=\operatorname{rk}_P(p)+\operatorname{rk}_Q(q). \end{align*} Using the definition of $F_{P\times Q}(t)$ and then substituting this rank formula, \begin{align*} F_{P\times Q}(t)=\sum_{(p,q)\in P\times Q}t^{\operatorname{rk}_{P\times Q}(p,q)}. \end{align*} Since summing over $P\times Q$ is the same as summing first over $P$ and then over $Q$, this becomes \begin{align*} F_{P\times Q}(t)=\sum_{p\in P}\sum_{q\in Q}t^{\operatorname{rk}_P(p)+\operatorname{rk}_Q(q)}. \end{align*} Since exponents add under multiplication, \begin{align*} t^{\operatorname{rk}_P(p)+\operatorname{rk}_Q(q)} = t^{\operatorname{rk}_P(p)}t^{\operatorname{rk}_Q(q)}. \end{align*} Because $P$ and $Q$ are finite, the double sum factors: \begin{align*} F_{P\times Q}(t)=\left(\sum_{p\in P}t^{\operatorname{rk}_P(p)}\right)\left(\sum_{q\in Q}t^{\operatorname{rk}_Q(q)}\right). \end{align*} By the definitions of $F_P(t)$ and $F_Q(t)$, this is \begin{align*} F_{P\times Q}(t)=F_P(t)F_Q(t). \end{align*} This proves both asserted product formulas. [/step]