Theorem: Quotient Epimorphism Condition for Normal Subgroup Product to be Internal Group Direct Product/Sufficient Condition

Let $\struct {G, \odot}$ be a group
Let $\struct {H, \odot}$ and $\struct {K, \odot}$ be normal subgroups of $\struct {G, \odot}$.
Let $\struct {G, \odot}$ be the internal group direct product of $\struct {H, \odot}$ and $\struct {K, \odot}$.
Then:
:the restriction of the quotient epimorphism $q_H$ to $K$ is an isomorphism from $K$ onto the quotient group $G / H$
and:
:the restriction of the quotient epimorphism $q_K$ to $H$ is an isomorphism from $H$ onto the quotient group $G / K$.

Proof:
Recall that the quotient epimorphism $q_H: G \to G / H$ is defined as:
:$\forall x \in G: \map {q_H} x = x \odot H$
From Restriction of Homomorphism is Homomorphism:
:the restriction of $q_H$ to $K$ is a homomorphism.
From Lagrange's Theorem (Group Theory):
:$\card {G / H} = \card K$
Then we have:
{{begin-eqn}}
{{eqn | q = \forall a, b \in K
      | l = \map {q_H} a
      | r = \map {q_H} b
      | c = by assumption
}}
{{eqn | ll= \leadsto
      | l = a \odot H
      | r = b \odot H
      | c = {{Defof|Quotient Group Epimorphism}}
}}
{{eqn | ll= \leadsto
      | q = \exists h, h' \in H
      | l = a \odot \paren {a^{-1} \odot h \odot a}
      | r = b \odot \paren {b^{-1} \odot h' \odot b}
      | c = as $H$ is a normal subgroup of $G$
}}
{{eqn | ll= \leadsto
      | l = h \odot a
      | r = h' \odot b
      | c = where $h, h' \in H$ and $a, b \in K$
}}
{{end-eqn}}
But by definition of internal group direct product, a representation of $g \in G$ in the form $h \odot k$ where $h \in H$ and $k \in K$ is unique.
That is:
{{begin-eqn}}
{{eqn | l = h
      | r = h'
}}
{{eqn | l = a
      | r = b
}}
{{end-eqn}}
Hence the restriction of $q_H$ to $K$ is an injection.
Hence by Injection to Equivalent Finite Set is Bijection, it follows that:
:$q_H$ is a bijection.
A bijective homomorphism is an isomorphism by definition.
{{qed|lemma}}
Similarly, the quotient epimorphism $q_K: G \to G / K$ is defined as:
:$\forall x \in G: \map {q_K} x = x \odot K = K \odot x$
as $K$ is a normal subgroup of $G$
From Restriction of Homomorphism is Homomorphism:
:the restriction of $q_K$ to $H$ is a homomorphism.
From Lagrange's Theorem (Group Theory):
:$\card {G / K} = \card H$
Then we have:
{{begin-eqn}}
{{eqn | q = \forall a, b \in K
      | l = \map {q_K} a
      | r = \map {q_K} b
      | c = by assumption
}}
{{eqn | ll= \leadsto
      | l = K \odot a
      | r = K \odot b
      | c = {{Defof|Quotient Group Epimorphism}}
}}
{{eqn | ll= \leadsto
      | q = \exists k, k' \in K
      | l = \paren {a \odot k \odot a^{-1} } \odot a
      | r = \paren {b \odot k' \odot b^{-1} } \odot b
      | c = as $K$ is a normal subgroup of $G$
}}
{{eqn | ll= \leadsto
      | l = a \odot k
      | r = b \odot k'
      | c = where $a, b \in H$ and $k, k' \in K$
}}
{{end-eqn}}
But by definition of internal group direct product, a representation of $g \in G$ in the form $h \odot k$ where $h \in H$ and $k \in K$ is unique.
That is:
{{begin-eqn}}
{{eqn | l = k
      | r = k'
}}
{{eqn | l = a
      | r = b
}}
{{end-eqn}}
Hence the restriction of $q_K$ to $H$ is an injection.
Hence by Injection to Equivalent Finite Set is Bijection, it follows that:
:$q_K$ is a bijection.
A bijective homomorphism is an isomorphism by definition.
Hence the result.