Dimension of Hilbert space tensor product Let $H_1, H_2$ be Hilbert spaces and consider their Hilbert space tensor product $$H_1 \hat{\otimes} H_2$$ which is the completion of the algebraic tensor product $H_1 \otimes H_2$ with respect to the unique inner product on $H_1 \otimes H_2$ satisfying $$\langle x \otimes y, x' \otimes y'\rangle = \langle x , x' \rangle \langle y, y'\rangle$$
If $E_1$ is an orthonormal basis for $H_1$ and $E_2$ is an orthonormal basis for $H_2$, I proved that $$E_1 \otimes E_2:= \{x \otimes y: x \in E_1, y\in E_2\}$$
is an orthonormal basis for $H_1 \hat{\otimes} H_2$. From this, I want to deduce that $$\dim(H_1 \hat{\otimes} H_2 ) = \dim (H_1) \dim (H_2)$$
(product of cardinal numbers). I see that it suffices to check that the map
$$E_1 \times E_2 \to E_1 \otimes E_2: (x,y) \mapsto x \otimes y$$
is injective, but I can't see why this holds:
$$x \otimes y = x' \otimes y' \implies x= x', y = y'$$
must not be true for general pure tensors, but maybe because we have the orthogonality we can say something more?
 A: Assume $(x,y)\ne (x',y')$ and consider a bilinear map $f:H_1\times H_2\to\Bbb C$ defined on the bases as
$$f(e_1,e_2)=\left\{\matrix{1&\text{ if }e_1=x\text{ and }e_2= y\\
0&\text{ otherwise.}}\right.$$
This factors through $H_1\otimes H_2$ thus distinguishing $x\otimes y$ and $x'\otimes y'$.
A: Hint: If $X,Y$ are vector spaces and $\{x_1,\dots,x_n\}\subset X$ is linearly independent, then $\sum_{i=1}^nx_i\otimes y_i=0$ implies that $y_i=0$ for all $i$.
In your case: suppose that $x\neq x'$ or $y\neq y'$. WLOG suppose that $x\neq x'$. If $x\otimes y=x'\otimes y'$, then $x\otimes y + x'\otimes(-y')=0$. Since $\{x,x'\}$ are linearly independent, this yields $y=-y'=0$, so $y=y'=0$, a contradiction, since $y,y'$ are unit vectors.
A: The way you should approach this ultimately depends on your definition of the (algebraic) tensor product.
One approach is as follows: it suffices to note that $x \otimes y = x' \otimes y'$ only if there exists a scalar $\alpha$ for which $\alpha x = x'$ and $y = \alpha y'$.  If $x',x$ are part of the same orthonormal basis, then they are either equal or fail to be multiples of each other. So, your map is indeed injective.
