Lemma used to prove $\left|HK\right|=\frac{\left|H\right|\left|K\right|}{\left|H \cap K\right|}$

group-theory set-partition

Consider the map $\varphi: H/H\cap K\longrightarrow HK/K$ by $h(H\cap K)\mapsto hK$.

  1. This is a well defined map by your lemma $\impliedby$.

  2. This map is injective by your lemma $\implies$.

  3. This map is surjective by definition of $HK$.

Therefore this is a natural one-to-one correspondence between these cosets, and the Product Formula follows immediately.

I happen to have written about this yesterday, so here's a link for you https://ml868.user.srcf.net/ExpositoryWritings/Groups3.pdf. There are a few typos I haven't fixed but I hope it is readable and somewhat inspiring.

Related

What is the combinatorial interpretation behind the recursive relation: $L(n,k+1)=\frac{n-k}{k\left(k+1\right)}L(n,k)$
Maximize y, minimize x on logarithmic growth curve
Closed form for $\left(-1\right)^{n}\sum_{k=0}^{n}\left(-1\right)^{k}\binom{n}{k}2^{\binom{k}{2}}$
Contraposition followed by universal conditionals
The binary relation $R:=\subseteq$ with $\operatorname{Domain}(R)=\operatorname{Codomain}(R)=\mathscr{P}(A)$?
From baby Hartshorne: showing the exterior of a circle is segment connected
What does Tate mean when he wrote "Higher dimensional class field theory" in the new preface to the Artin-Tate book and another question?
Completely metrizable implies $G_\delta$
Consequences of the Langlands program
Is the solution to this holiday puzzle unique?
Convergence in $L^p$ of $f_n$ implies convergence in $L^1$ of $|f_n|^p$ and $f_n^p$
are non-degenerate critical points always isolated?