$H$ and $K$ are two normal subgroups of group $G$, $H\cap K=\{1\}$, $G=HK$, how to prove $G$ is isomorphic to $H\times K$ If group $G$ has two normal subgroups $H$ and $K$ satisfying $H\cap K=\{1\}$ and $G=HK$, how to prove that $G$ is isomorphic to $H\times K$?
Since the factoring of any $g\in G$ as product $hk$ is unique under given conditions, I tried to prove that the map $\phi:G\ni g\mapsto (h,k)\in H\times K$ is the isomorphism. I can show that $\phi$ is a bijection. Next, I need to show it preserves group operation. Assuming $\forall g_1,g_2\in G$, $g_1=h_1k_1$ and $g_2=h_2k_2$ (the factoring is unique), we have $g_1g_2=h_1k_1h_2k_2$. But $\phi(g_1)=(h_1,k_1),\phi(g_2)=(h_2,k_2)$, so in product group $H\times K$, the operation $\phi(g_1)\phi(g_2)=(h_1h_2,k_1k_2)$. Its pre-image of $\phi$ in $G$ should be the  product $h_1h_2k_1k_2$. So we must establish $h_1k_1h_2k_2=h_1h_2k_1k_2$, which is equivalent to $k_1h_2=h_2k_1$. But I cannot prove this commutative relation based on the given conditions. The normality of $H$ implies $k_1^{-1}h_2k_1\in H$, but it does not necessarily equal $h_2$. This is where I got stuck. Is the above commutative relation true and how do I prove it? Or, was I wrong at the very beginning about what the isomorphism is? Could you please give me some help? Thank you.
 A: Hint. For $h ∈ H$, $k ∈ K$, you have $hk = kh \iff hkh^{-1}k^{-1} = 1$.
A: This doesn't add much to your excellent effort, other than some details.

For any pair of subgroups $H, K\le G$, the set $H\times K$ can be partitioned into equivalence classes all equicardinal to $H\cap K$, and such that $(H\times K)/\sim$ is equicardinal to $HK$. In fact:

Let's define in $H\times K$ the equivalence relation: $(h,k)\sim (h',k')\stackrel{(def.)}{\iff} hk=h'k'$. The equivalence class of $(h,k)$ is given by:
$$[(h,k)]_\sim=\{(h',k')\in H\times K\mid h'k'=hk\} \tag 1$$
Now define the following map from any equivalence class:
\begin{alignat*}{1}
  f_{(h,k)}:[(h,k)]_\sim &\longrightarrow&  H\cap K \\
  (h',k')&\longmapsto& f_{(h,k)}((h',k')):=k'k^{-1} \\
\tag 2
 \end{alignat*}
Note that $k'k^{-1}\in K$ by closure of $K$, and $k'k^{-1}\in H$ because $k'k^{-1}=h'^{-1}h$ (being $(h',k')\in [(h,k)]_\sim$) and by closure of $H$. Therefore, indeed $k'k^{-1}\in H\cap K$.
Lemma 1. $f_{(h,k)}$ is bijective.
Proof.
\begin{alignat}{2}
f_{(h,k)}((h',k'))=f_{(h,k)}((h'',k'')) &\space\space\space\Longrightarrow &&k'k^{-1}=k''k^{-1} \\
&\space\space\space\Longrightarrow &&k'=k'' \\
&\stackrel{h'k'=h''k''}{\Longrightarrow} &&h'=h'' \\
&\space\space\space\Longrightarrow &&(h',k')=(h'',k'') \\
\end{alignat}
and the map is injective. Then, for every $a\in H\cap K$, we  get $ak\in K$ and $a=f_{(h,k)}((h',ak))$, and the map is surjective. $\space\space\Box$
Now define the following map from the quotient set:
\begin{alignat}{1}
  f:(H\times K)/\sim &\longrightarrow&  HK \\
  [(h,k)]_\sim &\longmapsto& f([(h,k)]_\sim):=hk \\
\tag 3
 \end{alignat}
Lemma 2. $f$ is well-defined and bijective.
Proof.

*

*Good definition: $(h',k')\in [(h,k)]_\sim \Rightarrow f([(h',k')]_\sim)=h'k'=hk=f([(h,k)]_\sim)$;

*Injectivity: $f([(h',k')]_\sim)=f([(h,k)]_\sim) \Rightarrow h'k'=hk \Rightarrow (h',k')\in [(h,k)]_\sim \Rightarrow [(h',k')]_\sim=[(h,k)]_\sim$;

*Surjectivity: for every $ab\in HK$ , we get $ab=f([(a,b)]_\sim)$. $\space\space\Box$

As a corollary, if $|H\cap K|=1$, then all the classes $[(h,k)]_\sim$ are singletons, and hence the map $\tilde f\colon H\times K\to (H\times K)/\sim$, defined by $(h,k)\mapsto [(h,k)]_\sim$, is bijective; this, in turn, implies that the composite map $f\circ\tilde f\colon H\times K\to HK$ is bijective, too. If, in addition, $H\unlhd G$ and $K\unlhd G$, then for every $h\in H, k\in K$ we have that $hkh^{-1}k^{-1}\in H\cap K$, whence $hkh^{-1}k^{-1}=e$ and finally $hk=kh$. This, and the assumption $HK=G$, make of $f\circ\tilde f$ a (bijective) group homomorphism (namely an isomorphism). In fact:

\begin{alignat}{1}
(f\circ\tilde f)((h,k)(h',k')) &= (f\circ\tilde f)(hh',kk') \\
&= f(\tilde f(hh',kk')) \\
&= f([hh',kk']_\sim) \\
&= hh'kk' \\
&= hkh'k' \\
&= (hk)(h'k') \\
&= f([h,k]_\sim)f([h',k']_\sim) \\
&= f(\tilde f(h,k))f(\tilde f(h',k')) \\
&= ((f\circ\tilde f)(h,k))((f\circ\tilde f)(h',k')) \\
\end{alignat}
