Let $\mathcal{H}_A\otimes\mathcal{H}_B$ be a finite-dimensional bipartite Hilbert space, $P_A$ a positive semi-definite operator on $\mathcal{H}_A$, $P_B$ a positive semi-definite operator on $\mathcal{H}_B$, and $U_{AB}$ a unitary operator on $\mathcal{H}_A\otimes\mathcal{H}_B$. In some roundabout way involving integrals over the unitary group it seems I can prove the following inequality: $$\mathrm{tr}_A\left(\mathrm{tr}_B((P_A\otimes P_B)U_{AB})\mathrm{tr}_B((P_A\otimes P_B)U_{AB}^\dagger)\right)\leq\mathrm{tr}(P_A^2)\mathrm{tr}(P_B)^2.$$ I have been unable to find a more ``conventional'' proof of this inequality, e.g. using von Neumann's trace inequality or Holder's inequality, so I am curious if this is a known result or if someone can provide a proof which uses only linear algebra.