[proofplan]
We construct $\pi\odot\rho$ from the universal property of the algebraic [tensor product](/page/Tensor%20Product), using the bilinear map $(a,b)\mapsto \pi(a)\otimes\rho(b)$. The main point is then to check the algebraic operations on elementary tensors: multiplication follows from the product rule for tensor products of bounded operators, and the involution follows from the adjoint rule. Since every element of $A\odot B$ is a finite sum of elementary tensors, bilinearity and conjugate-linearity extend the identities to all of $A\odot B$.
[/proofplan]
[step:Construct the linear map from the bilinear operator tensor map]
For each $a\in A$ and $b\in B$, the operators $\pi(a)\in\mathcal{L}(H)$ and $\rho(b)\in\mathcal{L}(K)$ determine a bounded operator $\pi(a)\otimes\rho(b)\in\mathcal{L}(H\otimes K)$. Define
\begin{align*}
\Phi:A\times B\to \mathcal{L}(H\otimes K),\qquad (a,b)\mapsto \pi(a)\otimes\rho(b).
\end{align*}
The map $\Phi$ is complex bilinear because $\pi$ and $\rho$ are complex linear and the bounded-operator tensor product is bilinear in the two operator variables. By the universal property of the algebraic tensor product, there is a unique complex [linear map](/page/Linear%20Map)
\begin{align*}
\pi\odot\rho:A\odot B\to \mathcal{L}(H\otimes K)
\end{align*}
such that
\begin{align*}
(\pi\odot\rho)(a\otimes b)=\Phi(a,b)=\pi(a)\otimes\rho(b)
\end{align*}
for all $a\in A$ and $b\in B$. This proves well-definedness and uniqueness.
[/step]
[step:Verify multiplicativity on elementary tensors]
Let $a_1,a_2\in A$ and $b_1,b_2\in B$. For elementary Hilbert tensors $h\otimes k\in H\odot K$, the product rule for tensor products of bounded operators gives
\begin{align*}
((\pi(a_1)\otimes\rho(b_1))(\pi(a_2)\otimes\rho(b_2)))(h\otimes k)=(\pi(a_1)\pi(a_2)h)\otimes(\rho(b_1)\rho(b_2)k).
\end{align*}
Since $\pi$ and $\rho$ are homomorphisms,
\begin{align*}
\pi(a_1)\pi(a_2)=\pi(a_1a_2)
\end{align*}
and
\begin{align*}
\rho(b_1)\rho(b_2)=\rho(b_1b_2).
\end{align*}
Thus the two bounded operators
\begin{align*}
(\pi(a_1)\otimes\rho(b_1))(\pi(a_2)\otimes\rho(b_2))
\end{align*}
and
\begin{align*}
\pi(a_1a_2)\otimes\rho(b_1b_2)
\end{align*}
agree on the dense subspace $H\odot K\subset H\otimes K$, so they are equal. Therefore
\begin{align*}
(\pi\odot\rho)((a_1\otimes b_1)(a_2\otimes b_2))=(\pi\odot\rho)(a_1\otimes b_1)(\pi\odot\rho)(a_2\otimes b_2).
\end{align*}
[guided]
We first check multiplication in the simplest possible case, namely on elementary tensors. This is enough because the multiplication on $A\odot B$ is defined by bilinear extension from elementary products, and every element of $A\odot B$ is a finite sum of such tensors.
Take $a_1,a_2\in A$, $b_1,b_2\in B$, $h\in H$, and $k\in K$. The elementary tensor $h\otimes k$ belongs to the algebraic tensor product $H\odot K$, which is dense in the [Hilbert space](/page/Hilbert%20Space) tensor product $H\otimes K$. By the defining action of tensor products of bounded operators,
\begin{align*}
((\pi(a_1)\otimes\rho(b_1))(\pi(a_2)\otimes\rho(b_2)))(h\otimes k)=(\pi(a_1)\pi(a_2)h)\otimes(\rho(b_1)\rho(b_2)k).
\end{align*}
Because $\pi:A\to\mathcal{L}(H)$ and $\rho:B\to\mathcal{L}(K)$ are representations, they preserve multiplication. Hence
\begin{align*}
\pi(a_1)\pi(a_2)=\pi(a_1a_2)
\end{align*}
and
\begin{align*}
\rho(b_1)\rho(b_2)=\rho(b_1b_2).
\end{align*}
Substituting these identities into the previous formula gives
\begin{align*}
((\pi(a_1)\otimes\rho(b_1))(\pi(a_2)\otimes\rho(b_2)))(h\otimes k)=(\pi(a_1a_2)h)\otimes(\rho(b_1b_2)k).
\end{align*}
The right-hand side is exactly
\begin{align*}
(\pi(a_1a_2)\otimes\rho(b_1b_2))(h\otimes k).
\end{align*}
Thus the two bounded operators agree on $H\odot K$. Since $H\odot K$ is dense in $H\otimes K$ and bounded operators agreeing on a dense subspace agree everywhere, we obtain
\begin{align*}
(\pi(a_1)\otimes\rho(b_1))(\pi(a_2)\otimes\rho(b_2))=\pi(a_1a_2)\otimes\rho(b_1b_2).
\end{align*}
Using the defining formula for $\pi\odot\rho$ and the product rule
\begin{align*}
(a_1\otimes b_1)(a_2\otimes b_2)=a_1a_2\otimes b_1b_2
\end{align*}
in $A\odot B$, this becomes
\begin{align*}
(\pi\odot\rho)((a_1\otimes b_1)(a_2\otimes b_2))=(\pi\odot\rho)(a_1\otimes b_1)(\pi\odot\rho)(a_2\otimes b_2).
\end{align*}
[/guided]
[/step]
[step:Extend multiplicativity from elementary tensors to finite sums]
Let $x,y\in A\odot B$. Choose finite representations
\begin{align*}
x=\sum_{i=1}^{m}a_i\otimes b_i
\end{align*}
and
\begin{align*}
y=\sum_{j=1}^{n}c_j\otimes d_j
\end{align*}
with $m,n\in\mathbb N$, $a_i,c_j\in A$, and $b_i,d_j\in B$. By bilinearity of multiplication in $A\odot B$,
\begin{align*}
xy=\sum_{i=1}^{m}\sum_{j=1}^{n}(a_ic_j)\otimes(b_id_j).
\end{align*}
Using linearity of $\pi\odot\rho$ and the elementary tensor computation from the previous step,
\begin{align*}
(\pi\odot\rho)(xy)=\sum_{i=1}^{m}\sum_{j=1}^{n}(\pi(a_i)\pi(c_j))\otimes(\rho(b_i)\rho(d_j)).
\end{align*}
By distributivity of operator multiplication in $\mathcal{L}(H\otimes K)$, this equals
\begin{align*}
\left(\sum_{i=1}^{m}\pi(a_i)\otimes\rho(b_i)\right)\left(\sum_{j=1}^{n}\pi(c_j)\otimes\rho(d_j)\right).
\end{align*}
Therefore
\begin{align*}
(\pi\odot\rho)(xy)=(\pi\odot\rho)(x)(\pi\odot\rho)(y).
\end{align*}
[/step]
[step:Verify preservation of the involution]
Let $a\in A$ and $b\in B$. For $h,h'\in H$ and $k,k'\in K$, the Hilbert tensor product [inner product](/page/Inner%20Product) satisfies
\begin{align*}
((\pi(a)\otimes\rho(b))(h\otimes k),h'\otimes k')_{H\otimes K}=(\pi(a)h,h')_H(\rho(b)k,k')_K.
\end{align*}
Using the adjoint identities for $\pi(a)$ and $\rho(b)$, this becomes
\begin{align*}
(h,\pi(a)^*h')_H(k,\rho(b)^*k')_K.
\end{align*}
Since $\pi$ and $\rho$ are $*$-representations,
\begin{align*}
\pi(a)^*=\pi(a^*)
\end{align*}
and
\begin{align*}
\rho(b)^*=\rho(b^*).
\end{align*}
The preceding inner product identity first holds on elementary tensors and then, by finite linearity in each vector variable, on all pairs of vectors in $H\odot K$. Since $H\odot K$ is dense in $H\otimes K$ and both candidate adjoints are bounded operators, equality of the corresponding inner products on $H\odot K$ extends to all of $H\otimes K$. Hence
\begin{align*}
(\pi(a)\otimes\rho(b))^*=\pi(a^*)\otimes\rho(b^*).
\end{align*}
Using the involution on $A\odot B$, this gives
\begin{align*}
(\pi\odot\rho)((a\otimes b)^*)=(\pi\odot\rho)(a\otimes b)^*.
\end{align*}
Now let $x\in A\odot B$ and choose a finite representation
\begin{align*}
x=\sum_{i=1}^{m}\lambda_i(a_i\otimes b_i)
\end{align*}
with $m\in\mathbb N$, $\lambda_i\in\mathbb C$, $a_i\in A$, and $b_i\in B$. The involution on $A\odot B$ is conjugate-linear, so
\begin{align*}
x^*=\sum_{i=1}^{m}\overline{\lambda_i}(a_i\otimes b_i)^*.
\end{align*}
Using linearity of $\pi\odot\rho$, the elementary tensor identity, and conjugate-linearity of the adjoint on $\mathcal{L}(H\otimes K)$, we obtain
\begin{align*}
(\pi\odot\rho)(x^*)=\sum_{i=1}^{m}\overline{\lambda_i}(\pi\odot\rho)((a_i\otimes b_i)^*)
\end{align*}
and therefore
\begin{align*}
(\pi\odot\rho)(x^*)=\sum_{i=1}^{m}\overline{\lambda_i}(\pi\odot\rho)(a_i\otimes b_i)^*.
\end{align*}
By conjugate-linearity of the adjoint again,
\begin{align*}
\sum_{i=1}^{m}\overline{\lambda_i}(\pi\odot\rho)(a_i\otimes b_i)^*=\left(\sum_{i=1}^{m}\lambda_i(\pi\odot\rho)(a_i\otimes b_i)\right)^*.
\end{align*}
Thus
\begin{align*}
(\pi\odot\rho)(x^*)=(\pi\odot\rho)(x)^*.
\end{align*}
Therefore $\pi\odot\rho$ preserves the involution.
[/step]
[step:Conclude that the spatial product is a star homomorphism]
The map $\pi\odot\rho$ is linear by construction. The preceding steps show that it preserves multiplication and the involution on all of $A\odot B$. Therefore
\begin{align*}
\pi\odot\rho:A\odot B\to\mathcal{L}(H\otimes K)
\end{align*}
is a well-defined $*$-homomorphism satisfying
\begin{align*}
(\pi\odot\rho)(a\otimes b)=\pi(a)\otimes\rho(b)
\end{align*}
for every $a\in A$ and $b\in B$.
[/step]
