Short exact sequence split For groups $G$, $H$, and $K$, assume there exists a left-split short exact sequence: $$ 1 \rightarrow K \xrightarrow{\varphi} G \xrightarrow{\psi} H \rightarrow 1$$
Then $\varphi$ is an injective homomorphsim, $\psi$ is a surjective homomorphism, and ${\rm Im}(\varphi) = \ker(\psi)$. Furthermore, there exists a homomorphism $\pi: G \rightarrow K$ such that $\pi \circ \varphi = id_K$.
How can I show that these assumptions imply that
$H \triangleleft G, K \triangleleft G, G = HK,$ and $H \cap K = \{ 1 \}$?
 A: Before we begin, I would like to set forth the following general relations which we shall refer to in the course of our proof:

*

*For any group morphism $f \colon G \to G'$ and any subset $X \subseteq G$, we have that $f^{-1}\left[f[X]\right]=X\mathrm{Ker}f$.

*For any group morphism $f \colon G \to G'$ and any subgroup $H \leqslant G$, we have the following description for the kernel of the restriction: $\mathrm{Ker}f_{|H}=H \cap \mathrm{Ker}f$.

For convenience I will slightly alter the original notation. Consider the following exact sequence:
$$\{1\} \xrightarrow \ F \xrightarrow{f} E \xrightarrow{g} G \xrightarrow{} \{1\} \tag{*}
$$
of groups, where $f$ admits the retraction $h \colon E \to F$. Consider the subgroups $H\colon=\mathrm{Im}f=\mathrm{Ker}g \trianglelefteq E$ and $K\colon=\mathrm{Ker}h \trianglelefteq E$.
The relation $h \circ f=\mathbf{1}_F$ leads to $h[H]=F$, whence by taking inverse images through $h$ we derive $E=h^{-1}[F]=h^{-1}\left[h[H]\right]=HK$ (general relation 1).
Since by definition $\mathrm{Im}f \subseteq H$ we have $\mathbf{1}_F=h \circ f=h_{|H} \circ {}_{H|}f$ (for arbitrary map $k \colon A \to B$ with subsets $M \subseteq A$, $N \subseteq B$ such that $k[M] \subseteq N$, the symbol ${}_{N|}k_{|M}$ denotes the restriction of $k$ between $M$ and $N$). Being the restriction of a map to its image, ${}_{H|}f$ is surjective and since it is the restriction of an injection it continues to be injective. This means that ${}_{H|}f$ is an isomorphism and the previous relation entails that the restriction $h_{|H}=\left({}_{H|}f\right)^{-1}$ is the inverse isomorphism. In particular this means that $h_{|H}$ is injective and we thus have $\{1_E\}=\mathrm{Ker}h_{|H}=K \cap H$ (general relation 2).
At this point we have already established that $H$ and $K$ are mutually supplementary subgroups of $E$, hence $E \approx H \times K \hspace{3pt} (\mathbf{Gr})$. Since ${}_{H|}f$ is an isomorphism it is clear that $F \approx H \hspace{3pt} (\mathbf{Gr})$. Let us also inspect the relation between $K$ and $G$. As $g$ is surjective we have $G=g[E]=g[HK]=g[K]$ ($H$ being the kernel of $g$). Furthermore, $\mathrm{Ker}g_{|K}=H \cap K=\{1_E\}$, which means that the restriction $g_{|K}$ is an isomorphism as well and we thus have $K \approx G \hspace{3pt} (\mathbf{Gr})$.
The previous analysis shows that $E \approx F \times G \hspace{3pt} (\mathbf{Gr})$. Let us remark that given the context there is an explicit way of exhibiting an isomorphism not only between the forementioned groups, but actually between the extensions $(^*)$ given at the beginning and the one below:
$$\{1\} \xrightarrow{} F \xrightarrow{\iota} F \times G \xrightarrow{p} G \xrightarrow{} \{1\},$$
where $\iota$ is the canonical injection given by $\iota(x)=(x, 1_G)$ and $p$ the canonical projection onto the second factor. Let us consider the direct product in restricted sense (also known as the diagonal product) $\varphi\colon=h\underline{\times}g \in \mathrm{Hom}_{\mathbf{Gr}}(E, F \times G)$. It is straightforward to see that:

*

*$\varphi \circ f=(h \circ f) \underline{\times} (g \circ f)=\mathbf{1}_F \underline{\times} \mathbf{0}_{GF}=\iota$ (for arbitrary groups $G$ and $G'$ the symbol $\mathbf{0}_{G'G}$ denotes the null morphism from $G$ to $G'$, as the category of groups does indeed have null objects)

*$p \circ \varphi=g$ by definition of direct products in restricted sense.

This establishes the commutativity of the following diagram:

which means nothing else than that $\varphi$ is indeed a morphism of extensions, hence implicitly an isomorphism between $E$ and $F \times G$.
