Showing that $\lvert H K\rvert = \frac{| H\| K|}{ |H\cap K|}$ I have seen a proof that for two subgroups $H$ and $K$ of a finite group $G$,
$$
|H K| = \frac{| H\| K\rvert}{| H\cap K|}
$$
The proof counts the number of elements $hk$ that are the same as $h'k'$ for $h,h'\in H$ and $k,k'\in K$. I got confused with this proof.
My question is if there is another way to make things like this more clear. For example, I know that if one has a surjective homomorphism $f:G \to H$ then $\lvert G\rvert / \lvert \ker f\rvert = \lvert H\rvert$. That is, one can count the number of elements in something by essentially finding the order of the kernel of a map. This looks like what is going on with the product $HK$. But I guess that $HK$ in general isn't a group, so one can't talk about a group homomorphism.
Is there a way to find the "kernel" of a general function and get something like the first isomorphism theorem? All I would be interested in is how this can be used to count things.
 A: $H\times K$ acts on $G$ (on the right) via $g\cdot(h,k)=h^{-1}gk$. Then $HK$ is the orbit of the identity element $e$, and so its size is $|H\times K|/|S_e|$ where $S_e$ is the stabiliser of $e$. Then $S_e=\{(h,h):k\in H\cap K\}$.
This method can also count the general double coset $HxK$.
A: 
Lemma:  $\color{blue}{ H\times K/\mathcal R}$ has $n$ elements that is, 
  $\color{blue}{n= |H\times K/\mathcal R| }$ and we have,
  $$ \color{blue}{|HK|= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}} $$
  This is a consequence of  $E_1$ and $E_2$ see below for all the details.

Consider the map
\begin{split}
\phi :&& H\times K\to HK\\
&& (h,k)\mapsto hk
\end{split}
Clearly, $\phi $ is onto (surjective ). Now we consider the relation,
$$\color{red}{(h,k)\mathcal R(h',k')\Longleftrightarrow hk=h'k'\Longleftrightarrow \phi(h,k)=\phi(h',k')}$$
It is easy to check that $\mathcal R$ is an equivalent relation on $H\times K$.

Fact.I. Let denote by $[h,k]_\mathcal R$ the class of an element $(h,k) \in H\times K.$ 
  
  
  Let $n\in \mathbb N$ be the number of classes of $ H\times K$ with respect to $\mathcal R.$ Also we denote by $\color{blue}{ H\times K/\mathcal R}$ the set of class. Precisely we have, 
  $$\color{blue}{ H\times K/\mathcal R= \{[h_1,k_1]_\mathcal R, [h_2,k_2]_\mathcal R\cdots, [h_n,k_n]_\mathcal R\}} $$
  Where, $(h_j,k_j)_j$ is a set of representative class of $H\times K/\mathcal R $.


First Equality: We consider the $\overline{\phi}$ the quotient map of $\phi$ w.r.t $\mathcal R.$ defines as follows:
\begin{split}
\overline{\phi} :&& H\times K/\mathcal R \to HK\\
&& [h,k]_\mathcal R \mapsto  \phi(h,k) = hk
\end{split}


*

*$\overline{\phi} $ is well define since from the red line above we have, 


$$\color{red}{(h',k') \in [h,k]_\mathcal R\Longleftrightarrow (h,k)\mathcal R(h',k')\\\Longleftrightarrow hk=h'k'\Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}\tag{Eq}.$$
- It is also easy to check that $\overline{\phi}$ is one-to-one(injective) and Hence bijective since $\phi$ is onto.
 
$$\color{red}{[h',k']_\mathcal R = [h,k]_\mathcal R\Longleftrightarrow (h',k') \in [h,k]_\mathcal R \Longleftrightarrow \overline{\phi}([h,k]_\mathcal R)=\overline{\phi}([h',k']_\mathcal R)}$$

conclusion $\overline{\phi}$ is a bijection and therfore, 
  $$\color{blue}{n=|H\times K/\mathcal R| = |HK|}\tag{$E_1$} $$

we are jumping to the second equality, starting  from the following observation.

Fact. II  Since $\mathcal R$ is an equivalent relation, we know that $\color{red}{([h_j,k_j]_\mathcal R)_{1\le j\le n}}$ is a partition of $H\times K$ that is, 
  $$\color{red}{ |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R| }$$
  Claim:(see the proof Below)
  $$\color{red}{|[h_j,k_j]_\mathcal R| = |H\cap K|}$$

Second Equality: Since for any finte sets A and B we have $|A\times B| =|A|\times|B|,$ using the claim and the foregoing relations, we get that
$$\color{blue}{|H|\times|K| = |H\times K| = \sum_{j=1}^{n} |[h_j,k_j]_\mathcal R|  = \sum_{j=1}^{n} |H\cap K|   =|H\times K/\mathcal R||H\cap K|}$$

Then $$ \color{blue}{n= |H\times K/\mathcal R| =\frac{|H\|K|}{|H\cap K|}}\tag{$E_2$} $$

Proof of the claim:
Now we would like to investigate $|[h,k]_\mathcal R|$.
$$\color{blue}{(h',k')\in [h,k]_\mathcal R \Longleftrightarrow hk=h'k'\Longleftrightarrow h'^{-1}h=k'k^{-1}\in H\cap K .}$$

Consider the map
  \begin{split}
f :&& [h,k]_\mathcal R \to H\cap K\\
&& (h',k')\mapsto  h'^{-1}h=k'k^{-1}
\end{split}
  The above relation shows that $f$ is well defined as a map. We will show that $f$ is a bijective map to conclude.



*

*$f$ is onto(surjective): Let $s\in  H\cap K $. If we let
$ k' =  h s^{-1}~~~\text{and}~~~ k'=sk$
then $\color{red}{h'k' = hs^{-1} sk =hk\Longleftrightarrow (h',k')\mathcal R (h,k) \implies (h',k') \in  [h,k]_\mathcal R}$
and hence $$\color{red}{f(h',k')= f(hs^{-1}, sk)} = s.$$


this prove that $f$ is onto.


*

*$f$ is one-to-one(injective): let, $(a,b), (x,y)\in  [h,k]_\mathcal R $ such that $f(a,b)=f(x,y)$.
We have 
$f(a,b) =a^{-1}h =bk^{-1} ~~~~\text{and}~~~f(x,y) =x^{-1}h =yk^{-1}$


then, 
\begin{split}
f(a,b)=f(x,y)&\implies& \color{blue}{a^{-1}h =bk^{-1}} =\color{red}{x^{-1}h =yk^{-1}}\\
&\implies& \color{blue}{a^{-1}h =x^{-1}h} ~~~~\text{and}~~~~\color{red}{ bk^{-1}=yk^{-1}}\\
&\implies& \color{red}{a =x} ~~~~\text{and}~~~~\color{red}{ b=y}\\
\end{split}


This proves that $f$ is bijective,s then the claim follows
