Semidirect product of groups (awaiting review)

Suppose $H$ and $N$ are groups with operations $*_H$ and $*_N$ and $\phi:H\to \Aut(N)$ is a homomorphism to the automorphism group of $N$, then the set $N\times H$ with the operation \[ (n_1, h_1)*(n_2, h_2) = (n_1*_N \phi(h_1)(n_2), h_1 *_H h_2)\] is a group called a semidirect product of $H$ and $N$ denoted $N:H$ or $N\rtimes H$.

The group $N:H$ has subgroups \[ N' = \{(n,e)\mid n\in N\} \cong N\] and \[ H' = \{(e,h) \mid h\in H\} \cong H\] satisfying $N'\cap H'=\{(e,e)\}$, $N'H'=N:H$, and $N$ is a normal subgroup of $N:H$.

Conversely, if a group $G$ has a normal subgroup $N$ and a subgroup $H$ such that $N\cap H=\{e\}$ such that $N\cap H=\{e\}$ and $NH=G$, then $G\cong N:H$ for some function $\phi$.