Homology of an equivariant product I am struggling with checking the following fact:
$$
H_*(E\Sigma_n\times_{\Sigma_n}X^{\times n})\cong H_*(\Sigma_n;C_*(X)^{\otimes n}).
$$
But I am not sure how to start. It seems correct and I suppose that it comes from the fact, that $E\Sigma_n$ is a free $\Sigma_n$-space and a homology of a group is given by the homology of its classifying space. Any solutions or hints would be highly appreciated.
 A: Allow me to use the following lemma. 

Let $C, C'$ be chain complexes over a ring $R$ with an action of a finite group $G$ by chain maps (a $G$-chain complex). If $f: C \to C'$ is a $G$-equivariant quasi-isomorphism, then the induced map $H_*(G;C) \to H_*(G;C')$ is an isomorphism.

To prove this, recall how these homology groups are defined: first, you take a degreewise projective resolution of $C_k$, which becomes a bicomplex with $G$-action; you take the totalization $T(C)$ of this bicompelex, and then pass to $T(C) \otimes_{R[G]} R$. 
Now, the point is that the natural map $T(C) \to T(C')$ is also an equivariant quasi-isomorphism, and the key property of projective resolutions is that quasi-isomorphisms are in fact homotopy equivalences. So $T(C)$ and $T(C')$ are homotopy equivalent as chain complexes over $R[G]$; this implies that the natural map $T(C) \otimes_{R[G]} R \to T(C') \otimes_{R[G]} R$ is a homotopy equivalence as well.
We quickly apply this twice. First, the cross product map $C_*(X;R)^{\otimes n} \to C_*(X^n;R)$ is a $\Sigma_n$-equivariant quasi-isomorphism; it is clearly equivariant, and that it is a quasi-isomorphism is the Eilenberg-Zilber theorem. So we may as well take $H_*(\Sigma_n, C_*(X^n))$. Second, the natural projection map $E\Sigma_n \times X^n \to X^n$ is an equivariant map which is also a non-equivariant homotopy equivalence; this implies that the map $C_*(E\Sigma_n \times X^n) \to C_*(X^n)$ is an equivariant quasi-isomorphism.
So we have $$H_*(\Sigma_n; C_*(X)^{\otimes n}) \cong H_*(\Sigma_n; C_*(E\Sigma_n \times X^n)).$$
Now to apply one of the main philosophies of equivariant homology: 

Let $C$ be a $G$-chain complex which is (degreewise) projective over $R[G]$. Then $H_*(G;C) \cong H_*(C \otimes_{R[G]} R)$. 

That is, the equivariant homology is just given by taking the quotient. Of course, this is immediate from the definition above: a projective $R[G]$-module has itself as a projective resolution.
Now for any $G$-space $X$, the chain complex $C_*(EG \times X)$ is (degreewise) free over $R[G]$. This follows from covering space theory: the map $EG \times X \to (EG \times X)/G =: X_{hG}$ is a covering map, as the $G$-action on $EG \times X$ is free; therefore any map $\sigma: \Delta^k \to X_{hG}$ lifts to precisely $|G|$ maps $\sigma: \Delta^k \to EG \times X$, determined by the image of a single point in $\Delta^k$; any two are related by the action of a unique element of $G$. In particular, one finds that as an $R[G]$-module, we have $C_k(EG \times X;R) \cong R[G] \otimes_R C_k(X_{hG};R)$ and, of course, $C_k(X^{hG};R)$ is a free $R$-module.
Thus you conclude $$H_*(G; C_*(X)) \cong H_*(X_{hG}),$$ and in particular from the above, $$H_*(\Sigma_n; C_*(X)^{\otimes n}) \cong H_*(E\Sigma_n \times_{\Sigma_n} X^n).$$ This is the desired result.
