Reduction commutes with products

Product moment identity: for $(\xi ,\eta )\in \mathfrak{g}\oplus \mathfrak{h}$ and $(u,v)\in T_{(p,q)}(M\times N)$, [F2] and [F1] give $d({\mu }_M\oplus {\mu }_N{)}_{(p,q)}^{(\xi ,\eta )}(u,v)=d({\mu }_M^{\xi }{)}_p(u)+d({\mu }_N^{\eta }{)}_q(v)=-{\omega }_M({\xi }_M(p),u)-{\omega }_N({\eta }_N(q),v)=-\mathrm{\Omega }(({\xi }_M(p),{\eta }_N(q)),(u,v))\mathrm{.}$ Each factor action preserves its symplectic form, so the componentwise action preserves $\mathrm{\Omega }$ by the two pullback projections.

Equivariance: ${\mu }_{M\times N}((g,h)\cdot (p,q))={\mu }_M(g\cdot p)\oplus {\mu }_N(h\cdot q)=(g\cdot {\mu }_M(p))\oplus (h\cdot {\mu }_N(q))=(g,h)\cdot ({\mu }_M(p)\oplus {\mu }_N(q))$ by componentwise coadjoint action [F3].

The stabilizer action on ${\mu }_M^{-1}(\alpha )\times {\mu }_N^{-1}(\beta )$ is free: if $(g,h)$ fixes $(p,q)$, then $g$ fixes $p$ and $h$ fixes $q$, so $g=e$ and $h=e$. It is proper as well. Indeed, after permuting factors, its action map is the product of the two proper action maps. The inverse image of a compact set is a closed subset of the product of the inverse images of its compact coordinate projections, and is therefore compact.

Regularity: the differential of ${\mu }_{M\times N}$ at $(p,q)$ is $d({\mu }_M{)}_p\oplus d({\mu }_N{)}_q$, whose image is $\mathrm{im}d({\mu }_M{)}_p\oplus \mathrm{im}d({\mu }_N{)}_q$. Hence it is surjective if and only if both summands are, so the assumed regularity of both factor values proves regularity at every point of the product level. If either factor level is empty, the product level is empty and regularity is vacuous; no converse about factor regularity is asserted in that case.

Write $Z_M={\mu }_M^{-1}(\alpha )$, $Z_N={\mu }_N^{-1}(\beta )$ and $Z=Z_M\times Z_N$. Let $q_M:Z_M\to M_{\alpha }$, $q_N:Z_N\to N_{\beta }$ and $Q:Z\to Z\mathrm{/}(G_{\alpha }\times H_{\beta })$ be the quotient maps. By the verified hypotheses and [F4] these are smooth surjective submersions. The map $\varphi :([p],[q])\mapsto [(p,q)]$ is well defined and bijective, because product orbits are exactly products of the factor orbits. On neighbourhoods with local sections $s_M,s_N$ from [F4], it is $Q\circ (s_M\times s_N)$, hence smooth. Conversely, composing a local section $s$ of $Q$ with $(q_M\circ {\mathrm{pr}}_M,q_N\circ {\mathrm{pr}}_N)$ gives the inverse of $\varphi$ locally, hence that inverse is smooth. Put $P=q_M\times q_N$ and $j={\iota }_M\times {\iota }_N$. The defining reduced-form identities imply $P^{\ast }({\omega }_{\alpha }\oplus {\omega }_{\beta })=j^{\ast }\mathrm{\Omega }=Q^{\ast }{\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}$. Since $Q=\varphi \circ P$, this gives $P^{\ast }({\varphi }^{\ast }{\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}-({\omega }_{\alpha }\oplus {\omega }_{\beta }))=0$. Pullback by the surjective submersion $P$ is injective: at each target point choose a preimage and lift the tangent arguments by its surjective differential. Thus ${\varphi }^{\ast }{\omega }_{\mathrm{r}\mathrm{e}\mathrm{d}}={\omega }_{\alpha }\oplus {\omega }_{\beta }$, as required. If a level is empty, both quotients and the product are empty, and the same assertion is the unique empty diffeomorphism with its empty form.

Steps 1.1 and 1.2 show that ${\mu }_{M\times N}$ is an equivariant moment map; steps 2.1 and 1.3 verify the reduction hypotheses for the product; step 3.1 identifies the reduced symplectic form with the product form under the canonical diffeomorphism.