I am reading the proof of the associative property for a semidirect product given in Dummit and Foote, and I am trying to make sense of one line in particular. So, let $H$ and $K$ be groups and let $\varphi$ be a homomorphism from $K$ into $\text{Aut}(H)$. Let $G$ be the set of ordered pairs $(h,k)$ with $h\in H$ and $k\in K$, and define the multiplication as $$(h_1,k_1)(h_2,k_2)=(h_1k_1\cdot h_2,k_1k_2),$$ where "$\cdot$" denotes the action corresponding to $\varphi$. In the proof given for associativity, we have $((a,x)(b,y))(c,z)=(ax\cdot b, xy)(c,z)=(ax\cdot b(xy)\cdot c,xyz)=(ax\cdot bx\cdot (y\cdot c),xyz)=(ax\cdot(by\cdot c),xyz).$
The last equality confuses me. It looks like we are somehow "factoring out" the $x$, but what property of group actions allows this?
Since $\varphi$ is a homomorphism from $K$ into $\text{Aut}(H)$, $\varphi(x)$ is again a homomorphism. So we have $$\varphi(x)(ab)=\varphi(x)(a)\varphi(x)(b).$$ Also note that $$x\cdot a=\varphi(x)(a).$$ Now we can write $$ax\cdot bx\cdot (y\cdot c)=a\varphi(x)(b)\varphi(x)(y\cdot c)=a\varphi(x)(b(y\cdot c))=ax\cdot(by\cdot c).$$