[proofplan]
We first verify that the displayed formula really defines a left action of the direct product group $H \times K$ on the underlying set $G$. The key point is that the inverse in the second coordinate reverses multiplication, so the associativity axiom for a group action matches the product law in $H \times K$. Once the action is established, the orbit of an element $g \in G$ is computed directly, and the expression with $k^{-1}$ is converted into the usual double coset $HgK$ using the fact that inversion is a bijection on the subgroup $K$.
[/proofplan]
[step:Verify that the formula defines a left action of $H \times K$ on $G$]
Let $e$ denote the identity element of $G$. Since $H,K \le G$, the identity elements of $H$ and $K$ are both $e$. Define
\begin{align*}
\alpha : (H \times K) \times G &\to G \\
((h,k),g) &\mapsto h g k^{-1}.
\end{align*}
This map is well-defined because $h,g,k^{-1} \in G$ and $G$ is closed under multiplication.
We check the two axioms for a left [group action](/page/Group%20Action). For every $g \in G$,
\begin{align*}
\alpha((e,e),g) = e g e^{-1} = g.
\end{align*}
Now let $(h_1,k_1),(h_2,k_2) \in H \times K$ and $g \in G$. The product in $H \times K$ is componentwise, so
\begin{align*}
\alpha((h_1,k_1)(h_2,k_2),g)
&= \alpha((h_1h_2,k_1k_2),g) \\
&= h_1h_2 g (k_1k_2)^{-1} \\
&= h_1h_2 g k_2^{-1}k_1^{-1} \\
&= h_1(h_2 g k_2^{-1})k_1^{-1} \\
&= \alpha((h_1,k_1),\alpha((h_2,k_2),g)).
\end{align*}
Thus $\alpha$ defines a left action of $H \times K$ on $G$.
[guided]
Let $e$ denote the identity element of $G$. Since $H$ and $K$ are [subgroups](/page/Subgroup) of $G$, they contain the same identity element $e$, and they are closed under inverses and multiplication. We define the proposed action map as
\begin{align*}
\alpha : (H \times K) \times G &\to G \\
((h,k),g) &\mapsto h g k^{-1}.
\end{align*}
This is a well-defined map into $G$: if $h \in H$, $k \in K$, and $g \in G$, then $h \in G$, $k^{-1} \in K \le G$, and the product $h g k^{-1}$ lies in $G$ by closure of the group operation.
We now verify the two axioms in the definition of a left [group action](/page/Group%20Action). First, the identity element of the direct product group $H \times K$ is $(e,e)$. For every $g \in G$,
\begin{align*}
\alpha((e,e),g) = e g e^{-1} = e g e = g.
\end{align*}
So the identity of $H \times K$ acts as the identity map on $G$.
Second, we verify compatibility with multiplication in $H \times K$. Let $(h_1,k_1),(h_2,k_2) \in H \times K$ and let $g \in G$. The group law on $H \times K$ is componentwise, hence
\begin{align*}
(h_1,k_1)(h_2,k_2) = (h_1h_2,k_1k_2).
\end{align*}
Applying $\alpha$ gives
\begin{align*}
\alpha((h_1,k_1)(h_2,k_2),g)
&= \alpha((h_1h_2,k_1k_2),g) \\
&= h_1h_2 g (k_1k_2)^{-1}.
\end{align*}
The inverse of a product reverses order, so $(k_1k_2)^{-1}=k_2^{-1}k_1^{-1}$. Therefore
\begin{align*}
\alpha((h_1,k_1)(h_2,k_2),g)
&= h_1h_2 g k_2^{-1}k_1^{-1} \\
&= h_1(h_2 g k_2^{-1})k_1^{-1} \\
&= \alpha((h_1,k_1),\alpha((h_2,k_2),g)).
\end{align*}
This proves the compatibility axiom. Hence $\alpha$ is a left action of $H \times K$ on $G$.
[/guided]
[/step]
[step:Compute each orbit and rewrite it as the double coset $HgK$]
Fix $g \in G$. By the definition of an [orbit](/page/Orbit), the orbit of $g$ under the action $\alpha$ is
\begin{align*}
(H \times K)\cdot g
&= \{\alpha((h,k),g) : (h,k) \in H \times K\} \\
&= \{h g k^{-1} : h \in H,\ k \in K\}.
\end{align*}
Since $K$ is a subgroup of $G$, the inversion map
\begin{align*}
\iota_K : K &\to K \\
k &\mapsto k^{-1}
\end{align*}
is a bijection. Hence the set of all elements $k^{-1}$ with $k \in K$ is exactly $K$. Therefore
\begin{align*}
\{h g k^{-1} : h \in H,\ k \in K\}
&= \{h g \ell : h \in H,\ \ell \in K\} \\
&= HgK.
\end{align*}
Thus the orbit of $g$ is precisely the double coset $HgK$. Since $g \in G$ was arbitrary, the orbits of the action are exactly the subsets $HgK$ with $g \in G$.
[guided]
Fix an element $g \in G$. The [orbit](/page/Orbit) of $g$ under the action of $H \times K$ is, by definition, the set of all points obtained by acting on $g$ with elements of $H \times K$. Therefore
\begin{align*}
(H \times K)\cdot g
&= \{\alpha((h,k),g) : (h,k) \in H \times K\}.
\end{align*}
Using the definition of $\alpha$, this becomes
\begin{align*}
(H \times K)\cdot g
&= \{h g k^{-1} : h \in H,\ k \in K\}.
\end{align*}
The only difference between this expression and the usual double coset notation $HgK$ is that the right factor appears as $k^{-1}$ rather than $k$. Because $K$ is a subgroup, inversion preserves $K$: if $k \in K$, then $k^{-1} \in K$. Moreover inversion is its own inverse, so the map
\begin{align*}
\iota_K : K &\to K \\
k &\mapsto k^{-1}
\end{align*}
is a bijection. Consequently, as $k$ ranges over $K$, the element $k^{-1}$ also ranges over all of $K$. Renaming the element $k^{-1}$ as $\ell \in K$, we obtain
\begin{align*}
\{h g k^{-1} : h \in H,\ k \in K\}
&= \{h g \ell : h \in H,\ \ell \in K\}.
\end{align*}
By definition, the right-hand side is the double coset $HgK$:
\begin{align*}
HgK = \{h g \ell : h \in H,\ \ell \in K\}.
\end{align*}
Thus
\begin{align*}
(H \times K)\cdot g = HgK.
\end{align*}
Since $g \in G$ was arbitrary, every orbit has the form $HgK$, and every subset $HgK$ arises as the orbit of its representative $g$.
[/guided]
[/step]