Theorem: Factors of Internal Direct Product of Subsemigroups are Normal Subgroups

Let $\struct {G, \odot}$ be a group.
Let $\struct {H, \odot_H}$ and $\struct {K, \odot_K}$ be subsemigroups of $\struct {G, \odot}$.
Let $\struct {G, \odot}$ be the internal direct product of $\struct {H, \odot_H}$ and $\struct {K, \odot_K}$.
Then $\struct {H, \odot_H}$ and $\struct {K, \odot_K}$ are normal subgroups of $\struct {G, \odot}$.

Proof:
Let $\struct {G, \odot}$ be the internal direct product of $\struct {H, \odot_H}$ and $\struct {K, \odot_K}$.
Let $e$ denote the identity element of $\struct {G, \odot}$.
By definition of internal direct product, the mapping $\phi: H \times K \to G$ defined as:
:$\forall h \in H, k \in K: \map \phi {h, k} = h \odot k$
is an isomorphism from the (external) direct product $\struct {H, \odot {\restriction_H} } \times \struct {K, \odot {\restriction_K} }$ onto $\struct {G, \odot}$.
Let the symbol $\odot$ also be used for the operation induced on $H \times K$ by $\odot {\restriction_H}$ and $\odot {\restriction_K}$.
From Condition for Mapping between Structure and Cartesian Product of Substructures to be Bijection:
:every element of $G$ can be expressed uniquely as a product of the form $h \odot k$ such that $\tuple{h, k} \in H \times K$.
Hence:
:$G = \set {h \odot k: h \in H, k \in K}$
and so by definition of subset product:
:$G = H \odot K$
{{qed|lemma}}
Suppose $x \in H \cap K$.
We have:
{{begin-eqn}}
{{eqn | l = x = x \odot e
      | o = :
      | r = x \in H, e \in K
      | c = 
}}
{{eqn | l = x = e \odot x
      | o = :
      | r = e \in H, x \in K
      | c = 
}}
{{end-eqn}}
Thus we see that:
{{begin-eqn}}
{{eqn | l = \map \phi {x, e}
      | r = \map \phi {e, x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x, e}
      | r = \tuple {e, x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = e
      | c = 
}}
{{end-eqn}}
Thus:
:$H \cap K = \set e$
{{qed|lemma}}
In the following, the term '''unique representation''' of $x \in G$ will be used specifically to mean:
:the {{apriori}} unique representation $x = a \odot b$ where $a \in H$ and $b \in K$.
First we note that:
:$e \odot e = e$
is the '''unique representation''' of $e \in G$.
Let $h \in H$ be arbitrary.
Now consider $h^{-1} \in G$.
Let its '''unique representation''' be $x \odot y$.
Then we have:
{{begin-eqn}}
{{eqn | l = h
      | o = \in
      | r = H
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = h \odot e
      | r = h
      | c = is the '''unique representation''' of $h \in G$, as $e \in K$
}}
{{eqn | l = e
      | r = \paren {h \odot e} \odot \paren {x \odot y}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = \paren {h \odot x} \odot y
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {h \odot x}
      | r = e
      | c = {{apriori}}: $e \odot e$ is the '''unique representation''' of $e$
}}
{{eqn | ll= \land
      | l = y
      | r = e
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = h^{-1}
      | c = 
}}
{{eqn | o = \in
      | r = H
      | c = 
}}
{{end-eqn}}
Thus we see that:
:$h \in H \implies h^{-1} \in H$
Similarly, let $k \in K$ be arbitrary.
Now consider $k^{-1} \in G$.
Let its '''unique representation''' be $x \odot y$.
Then we have:
{{begin-eqn}}
{{eqn | l = k
      | o = \in
      | r = K
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = e \odot k
      | r = k
      | c = is the '''unique representation''' of $k \in G$, as $e \in K$
}}
{{eqn | l = e
      | r = \paren {x \odot y} \odot \paren {e \odot k}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = x \odot \paren {y \odot k}
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = \paren {y \odot k}
      | r = e
      | c = {{apriori}}: $e \odot e$ is the '''unique representation''' of $e$
}}
{{eqn | ll= \land
      | l = x
      | r = e
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = k^{-1}
      | c = 
}}
{{eqn | o = \in
      | r = K
      | c = 
}}
{{end-eqn}}
Thus we see that:
:$k \in K \implies k^{-1} \in K$
Now suppose $a, b \in H$.
We have:
{{begin-eqn}}
{{eqn | l = a \odot b
      | r = \paren {a \odot e} \odot \paren {b \odot e}
      | c = where $a \odot e$ and $b \odot e$ are the '''unique representations''' of $a$ and $b$
}}
{{eqn | r = \paren {a \odot \paren {e \odot b} } \odot e
      | c = {{Group-axiom|1}}
}}
{{eqn | r = \paren {a \odot b} \odot e
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Hence $\paren {a \odot b} \odot e$ is the '''unique representation''' of $a \odot b \in G$.
It follows that $a \odot b \in H$.
Hence:
:$a, b \in H \implies a \odot b \in H$
and $H$ is a subgroup of $G$ by the Two-Step Subgroup Test.
{{qed|lemma}}
Now suppose $c, d \in K$.
We have:
{{begin-eqn}}
{{eqn | l = c \odot d
      | r = \paren {e \odot c} \odot \paren {e \odot d}
      | c = where $e \odot c$ and $e \odot d$ are the '''unique representations''' of $c$ and $d$
}}
{{eqn | r = e \odot \paren {\paren {c \odot e} \odot d}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e \odot \paren {c \odot d}
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
Hence $e \odot \paren {c \odot d}$ is the '''unique representation''' of $c \odot d \in G$.
It follows that $c \odot d \in K$.
Hence:
:$c, d \in K \implies c \odot d \in K$
and $K$ is a subgroup of $G$ by the Two-Step Subgroup Test.
{{qed|lemma}}
Consolidating our gains, we have that:
:$(1): \quad \struct {H, \odot {\restriction_H} }$ and $\struct {K, \odot {\restriction_K} }$ are subgroups of the group $\struct {G, \odot}$
:$(2): \quad$ The mapping $\phi: H \times K \to G$ defined as:
:::::$\forall h \in H, k \in K: \map \phi {h, k} = h \odot k$
::::is an isomorphism from the (external) direct product $\struct {H, \odot {\restriction_H} } \times \struct {K, \odot {\restriction_K} }$ onto $\struct {G, \odot}$.
It follows from the Internal Direct Product Theorem that:
:$(1): \quad \struct {H, \circ {\restriction_H} }$ and $\struct {K, \circ {\restriction_K} }$ are both normal subgroups of $\struct {G, \circ}$
:$(2): \quad G$ is the subset product of $H$ and $K$, that is: $G = H \circ K$
:$(3): \quad$ $H \cap K = \set e$ where $e$ is the identity element of $G$.
and the result follows.
{{qed}}