Lemma: Haar purity

For a Haar unit vector in ${\mathbb{C}}^m\otimes {\mathbb{C}}^n$,

Proof. For $D=mn$, unitary invariance and symmetry give

where $\mathsf{F}$ swaps the two complete copies. The normalization follows by taking the trace. The purity swap test uses ${\mathsf{F}}_m\otimes I_{n^2}$. Its traces against $I$ and ${\mathsf{F}}_m\otimes {\mathsf{F}}_n$ are $m{n}^2$ and $m^{2}n$, respectively.