Solution (source code)

= Solution

Use the fact that $K$ is a <normal subgroup> to move a factor of $K$ past a factor of $H$. For $h_1,h_2\in H$ and $k_1,k_2\in K$,
$$
(h_1k_1)(h_2k_2)=h_1h_2(h_2^{-1}k_1h_2)k_2\in HK,
$$
while
$$
(hk)^{-1}=k^{-1}h^{-1}=h^{-1}(hk^{-1}h^{-1})\in HK.
$$
The <identity element> belongs to $HK$. Hence \b[$HK$ is a <subgroup>], by the <subgroup test>. This proves the <product of a subgroup with a normal subgroup> construction; $H$ need not be a <normal subgroup>.

For each $h\in H$, <conjugation> maps $K$ to itself and respects its multiplication. The inverse of $k\mapsto h^{-1}kh$ is $k\mapsto hkh^{-1}$, so both are <group automorphisms> of $K$.

\b[The printed formula requires a composition convention.] For the printed $\phi_h(k)=h^{-1}kh$, ordinary <function composition> gives
$$
\boxed{\phi_{h_1h_2}=\phi_{h_2}\circ\phi_{h_1}.}
$$
Indeed, $(h_1h_2)^{-1}k(h_1h_2)=h_2^{-1}(h_1^{-1}kh_1)h_2$. Thus the displayed assignment is a <group antihomomorphism> with the usual multiplication in the <automorphism group>. It is a <group homomorphism> if the <automorphisms> are written as right operators and multiplied in the corresponding reverse order; this is precisely why <right conjugation reverses composition>.

With the usual left <function composition>, the corresponding <group homomorphism> is instead
$$
\boxed{\psi:H\longrightarrow\operatorname{Aut}(K),\qquad\psi_h(k)=hkh^{-1}.}
$$
Direct expansion gives $\psi_{h_1h_2}(k)=h_1(h_2kh_2^{-1})h_1^{-1}=(\psi_{h_1}\circ\psi_{h_2})(k)$. This states the intended <conjugation action> without silently reversing the order in the printed formula.