# Proof of associativity of semidirect product

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).$$
Let $$(h_1, k_1), (h_2, k_2), (h_3, k_3) \in H \rtimes K$$. Then
$$((h_1, k_1)(h_2, k_2))(h_3, k_3)=(h_1(k_1 \cdot h_2), k_1k_2)(h_3, k_3)$$ $$((h_1, k_1)(h_2, k_2))(h_3, k_3)=((h_1(k_1 \cdot h_2))(k_1k_2 \cdot h_3), (k_1k_2)k_3)$$ $$((h_1, k_1)(h_2, k_2))(h_3, k_3)=((h_1(k_1 \cdot h_2))(k_1 \cdot (k_2 \cdot h_3)), k_1(k_2k_3))$$ $$((h_1, k_1)(h_2, k_2))(h_3, k_3)=(h_1(k_1\cdot h_2(k_2 \cdot h_3)), k_1(k_2k_3))$$ $$((h_1, k_1)(h_2, k_2))(h_3, k_3)=(h_1, k_1)(h_2(k_2 \cdot h_3), k_2k_3)$$ $$((h_1, k_1)(h_2, k_2))(h_3, k_3)=(h_1, k_1)((h_2, k_2)(h_3, k_3))$$